let D be set ; :: thesis:
thus ( D is finite implies ex p being FinSequence st D = rng p ) :: thesis:

given g being Function such that A1: rng g = D and
A2: dom g in omega ; :: according to FINSET_1:def 1 :: thesis:
reconsider n = dom g as Element of NAT by A2;
defpred S₂[ object , object ] means S₁[$2,$1];
A3: for x being object st x in Seg n holds
ex y being object st S₂[x,y]

let x be object ; :: thesis:
assume A4: x in Seg n ; :: thesis:
then reconsider x = x as Element of NAT ;
x >= 1 by A4, Th1;
then ex k being Nat st x = 1 + k by NAT_1:10;
hence ex y being object st S₂[x,y] ; :: thesis:

end;

consider f being Function such that
A5: dom f = Seg n and
A6: for x being object st x in Seg n holds
S₂[x,f . x] from CLASSES1:sch 1(A3);
A7: rng f = dom g

A8: n = { k where k is Nat : k < n } by AXIOMS:4;
thus rng f c= dom g :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A9: y in dom f and
A10: x = f . y by FUNCT_1:def 3;
consider k being Nat such that
A11: x = k and
A12: y = k + 1 by A5, A6, A9, A10;
k + 1 <= n by A5, A9, A12, Th1;
then k < n by NAT_1:13;
hence x in dom g by A8, A11; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in dom g ; :: thesis:
then consider k being Nat such that
A13: x = k and
A14: k < n by A8;
( 1 <= k + 1 & k + 1 <= n ) by A14, NAT_1:11, NAT_1:13;
then A15: k + 1 in Seg n ;
then ex k1 being Nat st
( f . (k + 1) = k1 & k + 1 = k1 + 1 ) by A6;
hence x in rng f by A5, A13, A15, FUNCT_1:def 3; :: thesis:

end;

then dom (g * f) = Seg n by A5, RELAT_1:27;
then reconsider p = g * f as FinSequence by Def2;
take p ; :: thesis:
thus D = rng p by A1, A7, RELAT_1:28; :: thesis:

end;

given p being FinSequence such that A16: D = rng p ; :: thesis:
consider n being Nat such that
A17: dom p = Seg n by Def2;
A18: n = { k where k is Nat : k < n } by AXIOMS:4;
A19: for x being object st x in n holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in n ; :: thesis:
then ex k being Nat st
( x = k & k < n ) by A18;
then reconsider k = x as Nat ;
take k + 1 ; :: thesis:
thus S₁[x,k + 1] ; :: thesis:

end;

consider f being Function such that
A20: dom f = n and
A21: for x being object st x in n holds
S₁[x,f . x] from CLASSES1:sch 1(A19);
take p * f ; :: according to FINSET_1:def 1 :: thesis:
A22: rng f = dom p

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A23: y in dom f and
A24: x = f . y by FUNCT_1:def 3;
consider k being Nat such that
A25: y = k and
A26: x = k + 1 by A20, A21, A23, A24;
ex m being Nat st
( k = m & m < n ) by A18, A20, A23, A25;
then ( 1 <= k + 1 & k + 1 <= n ) by NAT_1:11, NAT_1:13;
hence x in dom p by A17, A26; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A27: x in dom p ; :: thesis:
then reconsider x = x as Element of NAT ;
1 <= x by A17, A27, Th1;
then consider m being Nat such that
A28: x = 1 + m by NAT_1:10;
x <= n by A17, A27, Th1;
then m < n by A28, NAT_1:13;
then A29: m in n by A18;
then ex k being Nat st
( m = k & f . m = k + 1 ) by A21;
hence x in rng f by A20, A28, A29, FUNCT_1:def 3; :: thesis:

end;