let F be FinSequence-yielding FinSequence; :: thesis: for f being FinSequence holds card (doms (F ^ <*f*>)) = (card (doms F)) * (len f)
let f be FinSequence; :: thesis: card (doms (F ^ <*f*>)) = (card (doms F)) * (len f)
defpred S₁[ Nat] means for f being FinSequence st len f = $1 holds
card (doms (F ^ <*f*>)) = (card (doms F)) * (len f);
A1: S₁[ 0 ]

proof

let f be FinSequence; :: thesis: ( len f = 0 implies card (doms (F ^ <*f*>)) = (card (doms F)) * (len f) )
assume A2: len f = 0 ; :: thesis: card (doms (F ^ <*f*>)) = (card (doms F)) * (len f)
( 1 <= (len F) + 1 & len (F ^ <*f*>) = (len F) + 1 ) by FINSEQ_2:16, NAT_1:11;
then ( 1 + (len F) in dom (F ^ <*f*>) & (F ^ <*f*>) . (1 + (len F)) = f ) by FINSEQ_3:25;
then not F ^ <*f*> is non-empty by A2;
then doms (F ^ <*f*>) = {} by Th45;
hence card (doms (F ^ <*f*>)) = (card (doms F)) * (len f) by A2; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let f be FinSequence; :: thesis: ( len f = n + 1 implies card (doms (F ^ <*f*>)) = (card (doms F)) * (len f) )
assume A5: len f = n + 1 ; :: thesis: card (doms (F ^ <*f*>)) = (card (doms F)) * (len f)
set n1 = n + 1;
set fn = f | n;
set S = { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } ;
n < n + 1 by NAT_1:13;
then A6: len (f | n) = n by A5, FINSEQ_1:59;
f = (f | n) ^ <*(f . (n + 1))*> by A5, FINSEQ_3:55;
then A7: doms (F ^ <*f*>) = (doms (F ^ <*(f | n)*>)) \/ { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } by Th52;
defpred S₂[ object , object ] means for g being FinSequence st g = $1 holds
$2 = g ^ <*(1 + (len (f | n)))*>;
A8: for x being object st x in doms F holds
ex y being object st
( y in { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in doms F implies ex y being object st
( y in { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } & S₂[x,y] ) )
assume A9: x in doms F ; :: thesis: ex y being object st
( y in { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } & S₂[x,y] )
then consider p being FinSequence such that
A10: ( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) by Def8;
take p ^ <*(1 + (len (f | n)))*> ; :: thesis: ( p ^ <*(1 + (len (f | n)))*> in { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } & S₂[x,p ^ <*(1 + (len (f | n)))*>] )
thus ( p ^ <*(1 + (len (f | n)))*> in { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } & S₂[x,p ^ <*(1 + (len (f | n)))*>] ) by A10, A9; :: thesis: verum

end;

consider H being Function such that
A11: ( dom H = doms F & rng H c= { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } ) and
A12: for x being object st x in doms F holds
S₂[x,H . x] from FUNCT_1:sch 6(A8);
A13: H is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom H or not x2 in dom H or not H . x1 = H . x2 or x1 = x2 )
assume A14: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as FinSequence by A11, A14;
( H . x1 = x1 ^ <*(1 + (len (f | n)))*> & H . x2 = x2 ^ <*(1 + (len (f | n)))*> ) by A14, A11, A12;
hence x1 = x2 by FINSEQ_2:17, A14; :: thesis: verum

end;

{ (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } c= rng H

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } or s in rng H )
assume s in { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } ; :: thesis: s in rng H
then consider g being Element of doms F such that
A15: ( s = g ^ <*(1 + (len (f | n)))*> & g in doms F ) ;
H . g = s by A15, A12;
hence s in rng H by A15, A11, FUNCT_1:def 3; :: thesis: verum

end;

then rng H = { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } by A11;
then A16: card (doms F) = card { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } by A13, A11, CARD_1:70;
then reconsider S = { (f ^ <*(1 + (len (f | n)))*>) where f is Element of doms F : f in doms F } as finite set ;
doms (F ^ <*(f | n)*>) misses S

proof

assume doms (F ^ <*(f | n)*>) meets S ; :: thesis: contradiction
then consider x being object such that
A17: ( x in doms (F ^ <*(f | n)*>) & x in S ) by XBOOLE_0:3;
consider g being Element of doms F such that
A18: ( x = g ^ <*(1 + (len (f | n)))*> & g in doms F ) by A17;
A19: len g = len F by A18, Th47;
consider p being FinSequence such that
A20: ( p = x & len p = len (F ^ <*(f | n)*>) & ( for i being Nat st i in dom p holds
p . i in dom ((F ^ <*(f | n)*>) . i) ) ) by Def8, A17;
( 1 <= 1 + (len F) & len (F ^ <*(f | n)*>) = (len F) + 1 ) by FINSEQ_2:16, NAT_1:11;
then p . (1 + (len F)) in dom ((F ^ <*(f | n)*>) . (1 + (len F))) by FINSEQ_3:25, A20;
then 1 + (len (f | n)) <= len (f | n) by A20, A18, A19, FINSEQ_3:25;
hence contradiction by NAT_1:13; :: thesis: verum

end;

hence card (doms (F ^ <*f*>)) = (card (doms (F ^ <*(f | n)*>))) + (card (doms F)) by A16, A7, CARD_2:40
.= ((card (doms F)) * n) + (card (doms F)) by A6, A4
.= (card (doms F)) * (len f) by A5 ;
:: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence card (doms (F ^ <*f*>)) = (card (doms F)) * (len f) ; :: thesis: verum