defpred S₁[ set ] means ex t9 being Element of F₂() st
( t9 in F₃() & $1 = F₄(t9) & P₁[$1,t9] );
set c = { F₄(t9) where t9 is Element of F₂() : t9 in F₃() } ;
set c1 = { tt where tt is Element of F₁() : S₁[tt] } ;
A1: { tt where tt is Element of F₁() : S₁[tt] } c= { F₄(t9) where t9 is Element of F₂() : t9 in F₃() }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { tt where tt is Element of F₁() : S₁[tt] } or x in { F₄(t9) where t9 is Element of F₂() : t9 in F₃() } )
assume x in { tt where tt is Element of F₁() : S₁[tt] } ; :: thesis: x in { F₄(t9) where t9 is Element of F₂() : t9 in F₃() }
then ex tt being Element of F₁() st
( x = tt & ex t9 being Element of F₂() st
( t9 in F₃() & tt = F₄(t9) & P₁[tt,t9] ) ) ;
hence x in { F₄(t9) where t9 is Element of F₂() : t9 in F₃() } ; :: thesis: verum

end;

A2: { tt where tt is Element of F₁() : S₁[tt] } c= F₁() from FRAENKEL:sch 10();
A3: F₃() is finite ;
{ F₄(t9) where t9 is Element of F₂() : t9 in F₃() } is finite from FRAENKEL:sch 21(A3);
then reconsider c1 = { tt where tt is Element of F₁() : S₁[tt] } as Element of Fin F₁() by A1, A2, FINSUB_1:def 5;
take c1 ; :: thesis: for t being Element of F₁() holds
( t in c1 iff ex t9 being Element of F₂() st
( t9 in F₃() & t = F₄(t9) & P₁[t,t9] ) )
let t be Element of F₁(); :: thesis: ( t in c1 iff ex t9 being Element of F₂() st
( t9 in F₃() & t = F₄(t9) & P₁[t,t9] ) )
( t in c1 implies ex tt being Element of F₁() st
( t = tt & ex t9 being Element of F₂() st
( t9 in F₃() & tt = F₄(t9) & P₁[tt,t9] ) ) ) ;
hence ( t in c1 iff ex t9 being Element of F₂() st
( t9 in F₃() & t = F₄(t9) & P₁[t,t9] ) ) ; :: thesis: verum