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

proof

given g being Function such that A1: rng g = D and
A2: dom g in omega ; :: according to FINSET_1:def 1 :: thesis: ex p being FinSequence st D = rng p
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]

proof

let x be object ; :: thesis: ( x in Seg n implies ex y being object st S₂[x,y] )
assume A4: x in Seg n ; :: thesis: ex y being object st S₂[x,y]
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: verum

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

proof

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: dom g c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in dom g )
assume x in rng f ; :: thesis: x in dom g
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: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in rng f )
assume x in dom g ; :: thesis: x in rng f
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: verum

end;

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

end;

given p being FinSequence such that A16: D = rng p ; :: thesis: D is finite
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]

proof

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

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: ( rng (p * f) = D & dom (p * f) in omega )
A22: rng f = dom p

proof

thus rng f c= dom p :: according to XBOOLE_0:def 10 :: thesis: dom p c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in dom p )
assume x in rng f ; :: thesis: x in dom p
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: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom p or x in rng f )
assume A27: x in dom p ; :: thesis: x in rng f
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: verum

end;

hence rng (p * f) = D by A16, RELAT_1:28; :: thesis: dom (p * f) in omega
dom (p * f) = dom f by A22, RELAT_1:27;
hence dom (p * f) in omega by A20, ORDINAL1:def 12; :: thesis: verum