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 :: thesis: for x being object holds
( ( 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₁() } ) )

let x be object ; :: 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 :: thesis: for d1, d2 being Element of D st F₃(d1) = F₃(d2) holds
d1 = d2

let d1, d2 be Element of D; :: thesis: ( F₃(d1) = F₃(d2) implies d1 = d2 )
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 :: 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 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;