let f be Function; :: thesis: ( doms <*f*> = <*(dom f)*> & rngs <*f*> = <*(rng f)*> )
A1: ( dom (doms <*f*>) = dom <*f*> & dom <*(dom f)*> = Seg 1 ) by FINSEQ_1:38, FUNCT_6:def 2;
A2: <*f*> . 1 = f by FINSEQ_1:40;
A3: ( dom <*f*> = Seg 1 & {f} = {f} ) by FINSEQ_1:38;
A4: <*(rng f)*> . 1 = rng f by FINSEQ_1:40;
A5: now :: thesis: for x being object st x in {1} holds
(rngs <*f*>) . x = <*(rng f)*> . x
let x be object ; :: thesis: ( x in {1} implies (rngs <*f*>) . x = <*(rng f)*> . x )
assume A6: 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 A2, A4, A3, A6, FINSEQ_1:2, FUNCT_6:def 3; :: thesis: verum
end;
A7: <*(dom f)*> . 1 = dom f by FINSEQ_1:40;
now :: thesis: for x being object st x in {1} holds
(doms <*f*>) . x = <*(dom f)*> . x
let x be object ; :: thesis: ( x in {1} implies (doms <*f*>) . x = <*(dom f)*> . x )
assume A8: 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 A2, A7, A3, A8, FINSEQ_1:2, FUNCT_6:def 2; :: thesis: verum
end;
hence doms <*f*> = <*(dom f)*> by A1, A3, FINSEQ_1:2; :: thesis: rngs <*f*> = <*(rng f)*>
( dom (rngs <*f*>) = dom <*f*> & dom <*(rng f)*> = Seg 1 ) by FINSEQ_1:38, FUNCT_6:def 3;
hence rngs <*f*> = <*(rng f)*> by A3, A5, FINSEQ_1:2; :: thesis: verum