deffunc H₁( set ) -> set = F₅(($1 `1 ),($1 `2 ));
set M = { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) } ;
consider f being Function such that
A3: dom f = [:(F₃() /\ F₁()),(F₄() /\ F₂()):] and
A4: for y being set st y in [:(F₃() /\ F₁()),(F₄() /\ F₂()):] holds
f . y = H₁(y) from FUNCT_1:sch 3();
A5: dom f = [:F₃(),F₄():] /\ [:F₁(),F₂():] by A3, ZFMISC_1:123;
{ F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) } = f .: [:F₃(),F₄():]

proof

thus { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) } c= f .: [:F₃(),F₄():] :: according to XBOOLE_0:def 10 :: thesis: f .: [:F₃(),F₄():] c= { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) } or x in f .: [:F₃(),F₄():] )
assume x in { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) } ; :: thesis: x in f .: [:F₃(),F₄():]
then consider u being Element of F₁(), v being Element of F₂() such that
A6: x = F₅(u,v) and
A7: u in F₃() and
A8: v in F₄() ;
A9: [u,v] in [:F₃(),F₄():] by A7, A8, ZFMISC_1:106;
then A10: [u,v] in dom f by A5, XBOOLE_0:def 4;
A11: [u,v] `2 = v by MCART_1:7;
[u,v] `1 = u by MCART_1:7;
then f . u,v = F₅(u,v) by A3, A4, A10, A11;
hence x in f .: [:F₃(),F₄():] by A6, A9, A10, FUNCT_1:def 12; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: [:F₃(),F₄():] or x in { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) } )
assume x in f .: [:F₃(),F₄():] ; :: thesis: x in { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) }
then consider y being set such that
A12: y in dom f and
A13: y in [:F₃(),F₄():] and
A14: x = f . y by FUNCT_1:def 12;
reconsider y = y as Element of [:F₁(),F₂():] by A5, A12, XBOOLE_0:def 4;
A15: y = [(y `1 ),(y `2 )] by MCART_1:23;
then A16: y `1 in F<sub>3</sub>() by A13, ZFMISC_1:106;
A17: y `2 in F₄() by A13, A15, ZFMISC_1:106;
x = F₅((y `1 ),(y `2 )) by A3, A4, A12, A14;
hence x in { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) } by A16, A17; :: thesis: verum

end;

hence { F₅(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : ( u9 in F₃() & v9 in F₄() ) } is finite by A1, A2; :: thesis: verum