defpred S1[ set ] means ex t9 being Element of F2() st
( t9 in F3() & \$1 = F4(t9) & P1[\$1,t9] );
set c = { F4(t9) where t9 is Element of F2() : t9 in F3() } ;
set c1 = { tt where tt is Element of F1() : S1[tt] } ;
A1: { tt where tt is Element of F1() : S1[tt] } c= { F4(t9) where t9 is Element of F2() : t9 in F3() }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { tt where tt is Element of F1() : S1[tt] } or x in { F4(t9) where t9 is Element of F2() : t9 in F3() } )
assume x in { tt where tt is Element of F1() : S1[tt] } ; :: thesis: x in { F4(t9) where t9 is Element of F2() : t9 in F3() }
then ex tt being Element of F1() st
( x = tt & ex t9 being Element of F2() st
( t9 in F3() & tt = F4(t9) & P1[tt,t9] ) ) ;
hence x in { F4(t9) where t9 is Element of F2() : t9 in F3() } ; :: thesis: verum
end;
A2: { tt where tt is Element of F1() : S1[tt] } c= F1() from A3: F3() is finite ;
{ F4(t9) where t9 is Element of F2() : t9 in F3() } is finite from then reconsider c1 = { tt where tt is Element of F1() : S1[tt] } as Element of Fin F1() by ;
take c1 ; :: thesis: for t being Element of F1() holds
( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() & t = F4(t9) & P1[t,t9] ) )

let t be Element of F1(); :: thesis: ( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() & t = F4(t9) & P1[t,t9] ) )

( t in c1 implies ex tt being Element of F1() st
( t = tt & ex t9 being Element of F2() st
( t9 in F3() & tt = F4(t9) & P1[tt,t9] ) ) ) ;
hence ( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() & t = F4(t9) & P1[t,t9] ) ) ; :: thesis: verum