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

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

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

A3: now

let x be set ; :: thesis: ( ( x in { F₃(d) where d is Element of D : d in F₁() } implies x in { F₃(d) where d is Element of F₂() : d in F₁() } ) & ( x in { F₃(d) where d is Element of F₂() : d in F₁() } implies x in { F₃(d) where d is Element of D : d in F₁() } ) )

hereby :: thesis: ( x in { F₃(d) where d is Element of F₂() : d in F₁() } implies x in { F₃(d) where d is Element of D : d in F₁() } )

assume x in { F₃(d) where d is Element of D : d in F₁() } ; :: thesis: x in { F₃(d) where d is Element of F₂() : d in F₁() }
then ex d being Element of D st
( F₃(d) = x & d in F₁() ) ;
hence x in { F₃(d) where d is Element of F₂() : d in F₁() } by A1; :: thesis: verum

end;

hereby :: thesis: verum

assume x in { F₃(d) where d is Element of F₂() : d in F₁() } ; :: thesis: x in { F₃(d) where d is Element of D : d in F₁() }
then ex d being Element of F₂() st
( F₃(d) = x & d in F₁() ) ;
hence x in { F₃(d) where d is Element of D : d in F₁() } ; :: thesis: verum

end;

end;

A4: now

let d1, d2 be Element of D; :: thesis: ( F₃(d1) = F₃(d2) implies d1 = d2 )
( d1 in F₁() & d2 in F₁() ) ;
then reconsider d = d1, dd = d2 as Element of F₂() by A1;
assume F₃(d1) = F₃(d2) ; :: thesis: d1 = d2
then d = dd by A2;
hence d1 = d2 ; :: thesis: verum

end;

A5: F₁() c= D ;
F₁(),{ F₃(d) where d is Element of D : d in F₁() } are_equipotent from FUNCT_7:sch 4(A5, A4);
hence F₁(),{ F₃(d) where d is Element of F₂() : d in F₁() } are_equipotent by A3, TARSKI:2; :: thesis: verum

end;

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

now

consider a being 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 a in { F₃(d) where d is Element of F₂() : d in F₁() } ;
then ex d being Element of F₂() st
( a = F₃(d) & d in F₁() ) ;
hence contradiction by A6; :: thesis: verum

end;

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

end;

end;