defpred S1[ set , set , set ] means $3 = F4($2,$1,F5($1));
A4: for n being Nat st 1 <= n & n < F2() holds
for x being set ex y being set st S1[n,x,y] ;
consider f being FinSequence such that
A5: ( len f = F2() & ( f . 1 = F3() or F2() = 0 ) & ( for i being Nat st 1 <= i & i < F2() holds
S1[i,f . i,f . (i + 1)] ) ) from RECDEF_1:sch 3(A4);
 defpred S2[ Nat] means ( 1 <= $1 & $1 <= F2() implies f . $1 in F1() ^omega );
A6: S2[ 0 ] ;
A7: now :: thesis: for i being Nat st S2[i] holds
S2[i + 1]
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A8: S2[i] ; :: thesis: S2[i + 1]
thus S2[i + 1] :: thesis: verum
proof
assume A9: ( 1 <= i + 1 & i + 1 <= F2() ) ; :: thesis: f . (i + 1) in F1() ^omega
reconsider x = F5(i) as Element of F1() by A3, A9, NAT_1:13;
per cases ( i = 0 or i > 0 ) ;
suppose i = 0 ; :: thesis: f . (i + 1) in F1() ^omega
hence f . (i + 1) in F1() ^omega by A2, A5, A9, AFINSQ_1:def 7; :: thesis: verum
end;
suppose i > 0 ; :: thesis: f . (i + 1) in F1() ^omega
then A10: ( i >= 1 + 0 & i in NAT ) by NAT_1:13, ORDINAL1:def 12;
( f . (i + 1) = F4((f . i),i,x) & f . i is finite 0 -based array of F1() ) by A8, A10, A5, A9, NAT_1:13;
then f . (i + 1) is finite 0 -based array of F1() by A1, A9, A10, NAT_1:13;
hence f . (i + 1) in F1() ^omega by AFINSQ_1:def 7; :: thesis: verum
end;
end;
end;
end;
A11: for i being Nat holds S2[i] from NAT_1:sch 2(A6, A7);
 rng f c= F1() ^omega
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in F1() ^omega )
assume x in rng f ; :: thesis: x in F1() ^omega
then consider y being object such that
A12: ( y in dom f & x = f . y ) by FUNCT_1:def 3;
reconsider y = y as Nat by A12;
( 1 <= y & y <= F2() ) by A12, A5, FINSEQ_3:25;
hence x in F1() ^omega by A11, A12; :: thesis: verum
end;
then reconsider f = f as FinSequence of F1() ^omega by FINSEQ_1:def 4;
take f ; :: thesis: ( len f = F2() & ( f . 1 = F3() or F2() = 0 ) & ( for i being Nat st 1 <= i & i < F2() holds
f . (i + 1) = F4((f . i),i,F5(i)) ) )
thus ( len f = F2() & ( f . 1 = F3() or F2() = 0 ) ) by A5; :: thesis: for i being Nat st 1 <= i & i < F2() holds
f . (i + 1) = F4((f . i),i,F5(i))
let i be Nat; :: thesis: ( 1 <= i & i < F2() implies f . (i + 1) = F4((f . i),i,F5(i)) )
assume ( 1 <= i & i < F2() ) ; :: thesis: f . (i + 1) = F4((f . i),i,F5(i))
hence f . (i + 1) = F4((f . i),i,F5(i)) by A5; :: thesis: verum