deffunc H₁( object ) -> object = 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 object 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:100;
{ 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 object ; :: 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:87;
then A10: [u,v] in dom f by A5, XBOOLE_0:def 4;
A11: [u,v] `2 = v ;
[u,v] `1 = u ;
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 6; :: thesis: verum

end;

let x be object ; :: 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 object such that
A12: y in dom f and
A13: y in [:F₃(),F₄():] and
A14: x = f . y by FUNCT_1:def 6;
reconsider y = y as Element of [:F₁(),F₂():] by A5, A12, XBOOLE_0:def 4;
A15: y = [(y `1),(y `2)] by MCART_1:21;
then A16: y `1 in F<sub>3</sub>() by A13, ZFMISC_1:87;
A17: y `2 in F₄() by A13, A15, ZFMISC_1:87;
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₅(u,v) where u is Element of F₁(), v is Element of F₂() : ( u in F₃() & v in F₄() ) } is finite by A1, A2; :: thesis: verum