defpred S₁[ object , object ] means ex n being Nat st
( F = n & T = (canFS T) . (n + 1) );

A: now :: thesis: for x being object st x in card T holds
ex y being object st
( y in the carrier of F & S₁[x,y] )

let x be object ; :: thesis: ( x in card T implies ex y being object st
( y in the carrier of F & S₁[x,y] ) )
assume A1: x in card T ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )
then reconsider n = x as Ordinal ;
card n in card T by A1, CARD_1:9;
then n is finite by CARD_2:49;
then reconsider n = n as Nat ;
( 0 <= n & n < card T ) by A1, FIELD_5:3;
then ( 1 <= n + 1 & n + 1 <= card T ) by NAT_1:11, NAT_1:13;
then n + 1 in Seg (card T) by FINSEQ_1:1;
then n + 1 in Seg (len (canFS T)) by FINSEQ_1:93;
then n + 1 in dom (canFS T) by FINSEQ_1:def 3;
then A2: (canFS T) . (n + 1) in rng (canFS T) by FUNCT_1:3;
( rng (canFS T) c= T & T c= the carrier of F ) by FINSEQ_1:def 4;
then reconsider a = (canFS T) . (n + 1) as Element of F by A2;
thus ex y being object st
( y in the carrier of F & S₁[x,y] ) :: thesis: verum

proof

take a ; :: thesis: ( a in the carrier of F & S₁[x,a] )
thus ( a in the carrier of F & S₁[x,a] ) ; :: thesis: verum

end;

end;

consider f being Function of (card T), the carrier of F such that
B: for n being object st n in card T holds
S₁[n,f . n] from FUNCT_2:sch 1(A);

C: now :: thesis: for n being Nat st n in dom f holds
f . n = (canFS T) . (n + 1)

let n be Nat; :: thesis: ( n in dom f implies f . n = (canFS T) . (n + 1) )
assume n in dom f ; :: thesis: f . n = (canFS T) . (n + 1)
then consider i being Nat such that
C1: ( i = n & f . n = (canFS T) . (i + 1) ) by B;
thus f . n = (canFS T) . (n + 1) by C1; :: thesis: verum

end;

D: now :: thesis: for n being object st n in dom f holds
n is Nat

let n be object ; :: thesis: ( n in dom f implies n is Nat )
assume n in dom f ; :: thesis: n is Nat
then consider i being Nat such that
D1: ( i = n & f . n = (canFS T) . (i + 1) ) by B;
thus n is Nat by D1; :: thesis: verum

end;

take f ; :: thesis: f is T -evaluating
G: rng f c= T

proof

now :: thesis: for o being object st o in rng f holds
o in T

let o be object ; :: thesis: ( o in rng f implies o in T )
assume o in rng f ; :: thesis: o in T
then consider n being object such that
D1: ( n in dom f & f . n = o ) by FUNCT_1:def 3;
reconsider n = n as Nat by D1, D;
D2: f . n = (canFS T) . (n + 1) by D1, C;
D3: dom (canFS T) = Seg (len (canFS T)) by FINSEQ_1:def 3
.= Seg (card T) by FINSEQ_1:93 ;
n < card T by D1, FIELD_5:3;
then ( 1 <= n + 1 & n + 1 <= card T ) by NAT_1:12, NAT_1:13;
then D4: (canFS T) . (n + 1) in rng (canFS T) by D3, FINSEQ_1:1, FUNCT_1:3;
rng (canFS T) c= T by FINSEQ_1:def 4;
hence o in T by D1, D2, D4; :: thesis: verum

end;

hence rng f c= T ; :: thesis: verum

end;

E: f is one-to-one

proof

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume E1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider n1 = x1, n2 = x2 as Nat by D;
E2: (canFS T) . (n1 + 1) = f . n2 by E1, C
.= (canFS T) . (n2 + 1) by E1, C ;
E3: dom (canFS T) = Seg (len (canFS T)) by FINSEQ_1:def 3
.= Seg (card T) by FINSEQ_1:93 ;
n1 < card T by E1, FIELD_5:3;
then ( 1 <= n1 + 1 & n1 + 1 <= card T ) by NAT_1:12, NAT_1:13;
then E4: n1 + 1 in dom (canFS T) by E3, FINSEQ_1:1;
n2 < card T by E1, FIELD_5:3;
then ( 1 <= n2 + 1 & n2 + 1 <= card T ) by NAT_1:12, NAT_1:13;
then n2 + 1 in dom (canFS T) by E3, FINSEQ_1:1;
then n1 + 1 = n2 + 1 by E4, E2, FUNCT_1:def 4;
hence x1 = x2 ; :: thesis: verum

end;

hence f is one-to-one ; :: thesis: verum

end;

now :: thesis: for o being object st o in T holds
o in rng f

let o be object ; :: thesis: ( o in T implies o in rng f )
assume o in T ; :: thesis: o in rng f
then o in rng (canFS T) by FUNCT_2:def 3;
then consider n being object such that
F2: ( n in dom (canFS T) & (canFS T) . n = o ) by FUNCT_1:def 3;
F3: dom (canFS T) = Seg (len (canFS T)) by FINSEQ_1:def 3
.= Seg (card T) by FINSEQ_1:93 ;
reconsider n = n as Nat by F2;
F4: ( 1 <= n & n <= card T ) by F2, F3, FINSEQ_1:1;
then reconsider n1 = n - 1 as Nat ;
n1 + 1 = n ;
then n1 < card T by F4, NAT_1:13;
then n1 in card T by FIELD_5:3;
then F5: n1 in dom f by FUNCT_2:def 1;
then f . n1 = (canFS T) . (n1 + 1) by C
.= o by F2 ;
hence o in rng f by F5, FUNCT_1:def 3; :: thesis: verum

end;

then T c= rng f ;
hence f is T -evaluating by E, G, XBOOLE_0:def 10; :: thesis: verum