let f be Function; :: thesis: ( doms <*f*> = <*(dom f)*> & rngs <*f*> = <*(rng f)*> )
A1: ( rng <*f*> = {f} & <*f*> " (rng <*f*>) = dom <*f*> ) by FINSEQ_1:38, RELAT_1:134;
A2: ( dom (doms <*f*>) = <*f*> " (SubFuncs (rng <*f*>)) & dom <*(dom f)*> = Seg 1 ) by FINSEQ_1:38, FUNCT_6:def 2;
A3: <*f*> . 1 = f by FINSEQ_1:40;
A4: ( dom <*f*> = Seg 1 & SubFuncs {f} = {f} ) by FINSEQ_1:38, FUNCT_6:20;
A5: <*(rng f)*> . 1 = rng f by FINSEQ_1:40;

A6: now

let x be set ; :: thesis: ( x in {1} implies (rngs <*f*>) . x = <*(rng f)*> . x )
assume A7: x in {1} ; :: thesis: (rngs <*f*>) . x = <*(rng f)*> . x
then x = 1 by TARSKI:def 1;
hence (rngs <*f*>) . x = <*(rng f)*> . x by A1, A3, A5, A4, A7, FINSEQ_1:2, FUNCT_6:def 3; :: thesis: verum

end;

A8: <*(dom f)*> . 1 = dom f by FINSEQ_1:40;

now

let x be set ; :: thesis: ( x in {1} implies (doms <*f*>) . x = <*(dom f)*> . x )
assume A9: x in {1} ; :: thesis: (doms <*f*>) . x = <*(dom f)*> . x
then x = 1 by TARSKI:def 1;
hence (doms <*f*>) . x = <*(dom f)*> . x by A1, A3, A8, A4, A9, FINSEQ_1:2, FUNCT_6:def 2; :: thesis: verum

end;

hence doms <*f*> = <*(dom f)*> by A1, A2, A4, FINSEQ_1:2, FUNCT_1:2; :: thesis: rngs <*f*> = <*(rng f)*>
( dom (rngs <*f*>) = <*f*> " (SubFuncs (rng <*f*>)) & dom <*(rng f)*> = Seg 1 ) by FINSEQ_1:38, FUNCT_6:def 3;
hence rngs <*f*> = <*(rng f)*> by A1, A4, A6, FINSEQ_1:2, FUNCT_1:2; :: thesis: verum