per cases ( F₁() = {} or F₁() <> {} ) ;

suppose A3: F₁() = {} ; :: thesis: { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite

now :: thesis: not { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } <> {}

set a = the Element of { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } ;
assume { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } <> {} ; :: thesis: contradiction
then the Element of { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } ;
then ex d being Element of F₂() st
( the Element of { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } = F₃(d) & F₄(d) in F₁() ) ;
hence contradiction by A3; :: thesis: verum

end;

hence { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite ; :: thesis: verum

end;

suppose F₁() <> {} ; :: thesis: { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite

then reconsider D = F₁() as non empty set ;
defpred S₁[ set ] means ex d being Element of F₂() st $1 = F₄(d);
set B = { d where d is Element of F₂() : F₄(d) in D } ;
set C = { a where a is Element of D : S₁[a] } ;
A4: { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } = { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } }

proof

thus { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } c= { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } :: according to XBOOLE_0:def 10 :: thesis: { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } c= { F₃(d) where d is Element of F₂() : F₄(d) in F₁() }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } or x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } )
assume x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } ; :: thesis: x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } }
then consider d9 being Element of F₂() such that
A5: x = F₃(d9) and
A6: F₄(d9) in F₁() ;
d9 in { d where d is Element of F₂() : F₄(d) in D } by A6;
hence x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } by A5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } or x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } )
assume x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } ; :: thesis: x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() }
then consider d1 being Element of F₂() such that
A7: x = F₃(d1) and
A8: d1 in { d where d is Element of F₂() : F₄(d) in D } ;
ex d3 being Element of F₂() st
( d3 = d1 & F₄(d3) in D ) by A8;
hence x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } by A7; :: thesis: verum

end;

A9: { a where a is Element of D : S₁[a] } , { d where d is Element of F₂() : F₄(d) in D } are_equipotent

proof

take Z = { [F₄(d),d] where d is Element of F₂() : verum } ; :: according to TARSKI:def 6 :: thesis: ( ( for b₁ being object holds
( not b₁ in { a where a is Element of D : S₁[a] } or ex b₂ being object st
( b₂ in { d where d is Element of F₂() : F₄(d) in D } & [b₁,b₂] in Z ) ) ) & ( for b₁ being object holds
( not b₁ in { d where d is Element of F₂() : F₄(d) in D } or ex b₂ being object st
( b₂ in { a where a is Element of D : S₁[a] } & [b₂,b₁] in Z ) ) ) & ( for b₁, b₂, b₃, b₄ being object holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

hereby :: thesis: ( ( for b₁ being object holds
( not b₁ in { d where d is Element of F₂() : F₄(d) in D } or ex b₂ being object st
( b₂ in { a where a is Element of D : S₁[a] } & [b₂,b₁] in Z ) ) ) & ( for b₁, b₂, b₃, b₄ being object holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

let x be object ; :: thesis: ( x in { a where a is Element of D : S₁[a] } implies ex d being object st
( d in { d where d is Element of F₂() : F₄(d) in D } & [x,d] in Z ) )
assume x in { a where a is Element of D : S₁[a] } ; :: thesis: ex d being object st
( d in { d where d is Element of F₂() : F₄(d) in D } & [x,d] in Z )
then consider a being Element of D such that
A10: a = x and
A11: ex d being Element of F₂() st a = F₄(d) ;
consider d being Element of F₂() such that
A12: a = F₄(d) by A11;
reconsider d = d as object ;
take d = d; :: thesis: ( d in { d where d is Element of F₂() : F₄(d) in D } & [x,d] in Z )
thus ( d in { d where d is Element of F₂() : F₄(d) in D } & [x,d] in Z ) by A10, A12; :: thesis: verum

end;

hereby :: thesis: for b₁, b₂, b₃, b₄ being object holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) )

let y be object ; :: thesis: ( y in { d where d is Element of F₂() : F₄(d) in D } implies ex x being object st
( x in { a where a is Element of D : S₁[a] } & [x,y] in Z ) )
assume y in { d where d is Element of F₂() : F₄(d) in D } ; :: thesis: ex x being object st
( x in { a where a is Element of D : S₁[a] } & [x,y] in Z )
then consider d being Element of F₂() such that
A13: ( d = y & F₄(d) in D ) ;
reconsider x = F₄(d) as object ;
take x = x; :: thesis: ( x in { a where a is Element of D : S₁[a] } & [x,y] in Z )
thus ( x in { a where a is Element of D : S₁[a] } & [x,y] in Z ) by A13; :: thesis: verum

end;

let x, y, z, u be object ; :: thesis: ( not [x,y] in Z or not [z,u] in Z or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
assume [x,y] in Z ; :: thesis: ( not [z,u] in Z or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
then consider d1 being Element of F₂() such that
A14: [x,y] = [F₄(d1),d1] ;
assume [z,u] in Z ; :: thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )
then consider d2 being Element of F₂() such that
A15: [z,u] = [F₄(d2),d2] ;
A16: ( z = F₄(d2) & u = d2 ) by A15, XTUPLE_0:1;
( x = F₄(d1) & y = d1 ) by A14, XTUPLE_0:1;
hence ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, A16; :: thesis: verum

end;

{ a where a is Element of D : S₁[a] } is Subset of D from DOMAIN_1:sch 7();
then { a where a is Element of D : S₁[a] } is finite by A1, FINSET_1:1;
then A17: { d where d is Element of F₂() : F₄(d) in D } is finite by A9, CARD_1:38;
{ F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } is finite from FRAENKEL:sch 21(A17);
hence { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite by A4; :: thesis: verum

end;

end;