let g be FinSequence; :: thesis: card (doms <*g*>) = len g
set G = <*g*>;
A1: len <*g*> = 1 by FINSEQ_1:40;
defpred S₁[ object , object ] means for f being FinSequence st f = $1 holds
f . 1 = $2;
A2: for x being object st x in doms <*g*> holds
ex y being object st
( y in dom g & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in doms <*g*> implies ex y being object st
( y in dom g & S₁[x,y] ) )
assume A3: x in doms <*g*> ; :: thesis: ex y being object st
( y in dom g & S₁[x,y] )
then consider p being FinSequence such that
A4: ( p = x & len p = len <*g*> & ( for i being Nat st i in dom p holds
p . i in dom (<*g*> . i) ) ) by Def8;
take p . 1 ; :: thesis: ( p . 1 in dom g & S₁[x,p . 1] )
thus ( p . 1 in dom g & S₁[x,p . 1] ) by A4, A3, Th51; :: thesis: verum

end;

consider F being Function such that
A5: ( dom F = doms <*g*> & rng F c= dom g ) and
A6: for x being object st x in doms <*g*> holds
S₁[x,F . x] from FUNCT_1:sch 6(A2);
A7: F is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )
assume A8: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: x1 = x2
consider p1 being FinSequence such that
A9: ( p1 = x1 & len p1 = len <*g*> & ( for i being Nat st i in dom p1 holds
p1 . i in dom (<*g*> . i) ) ) by A5, A8, Def8;
consider p2 being FinSequence such that
A10: ( p2 = x2 & len p2 = len <*g*> & ( for i being Nat st i in dom p2 holds
p2 . i in dom (<*g*> . i) ) ) by A5, A8, Def8;
A11: ( p1 = <*(p1 . 1)*> & p2 = <*(p2 . 1)*> ) by A1, A9, A10, FINSEQ_1:40;
( F . x1 = p1 . 1 & F . x2 = p2 . 1 ) by A9, A10, A6, A5, A8;
hence x1 = x2 by A11, A8, A9, A10; :: thesis: verum

end;

dom g c= rng F

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in dom g or i in rng F )
assume A12: i in dom g ; :: thesis: i in rng F
A13: ( len <*i*> = 1 & <*i*> . 1 = i ) by FINSEQ_1:40;
then A14: <*i*> in doms <*g*> by Th51, A12;
F . <*i*> = <*i*> . 1 by A6, Th51, A12, A13;
hence i in rng F by A14, A5, FUNCT_1:def 3; :: thesis: verum

end;

then dom g = rng F by A5;
then card (doms <*g*>) = card (dom g) by A5, A7, CARD_1:70;
then card (doms <*g*>) = card (Seg (len g)) by FINSEQ_1:def 3;
hence card (doms <*g*>) = len g ; :: thesis: verum