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

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

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

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

end;

hence F₁(), { F₃(d) where d is Element of F₂() : d in F₁() } are_equipotent by A3; :: thesis: verum

end;

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

then reconsider A = F₁() as non empty set ;
set D = { F₃(d) where d is Element of F₂() : d in A } ;
A, { F₃(d) where d is Element of F₂() : d in A } are_equipotent

proof

take Z = { [d,F₃(d)] where d is Element of F₂() : verum } ; :: according to TARSKI:def 6 :: thesis: ( ( for b₁ being object holds
( not b₁ in A or ex b₂ being object st
( b₂ in { F₃(d) where d is Element of F₂() : d in A } & [b₁,b₂] in Z ) ) ) & ( for b₁ being object holds
( not b₁ in { F₃(d) where d is Element of F₂() : d in A } or ex b₂ being object st
( b₂ in 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 { F₃(d) where d is Element of F₂() : d in A } or ex b₂ being object st
( b₂ in 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 implies ex y being object st
( y in { F₃(d) where d is Element of F₂() : d in A } & [x,y] in Z ) )
assume A4: x in A ; :: thesis: ex y being object st
( y in { F₃(d) where d is Element of F₂() : d in A } & [x,y] in Z )
then reconsider d = x as Element of F₂() by A1;
reconsider y = F₃(d) as object ;
take y = y; :: thesis: ( y in { F₃(d) where d is Element of F₂() : d in A } & [x,y] in Z )
thus y in { F₃(d) where d is Element of F₂() : d in A } by A4; :: thesis: [x,y] in Z
thus [x,y] in Z ; :: 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 { F₃(d) where d is Element of F₂() : d in A } implies ex d being object st
( d in A & [d,y] in Z ) )
assume y in { F₃(d) where d is Element of F₂() : d in A } ; :: thesis: ex d being object st
( d in A & [d,y] in Z )
then consider d being Element of F₂() such that
A5: ( F₃(d) = y & d in A ) ;
reconsider d = d as object ;
take d = d; :: thesis: ( d in A & [d,y] in Z )
thus ( d in A & [d,y] in Z ) by A5; :: 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
A6: [x,y] = [d1,F₃(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
A7: [z,u] = [d2,F₃(d2)] ;
A8: ( z = d2 & u = F₃(d2) ) by A7, XTUPLE_0:1;
( x = d1 & y = F₃(d1) ) by A6, XTUPLE_0:1;
hence ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, A8; :: thesis: verum

end;

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

end;

end;