deffunc H1( object ) -> object = F5(($1 `1),($1 `2));
set M = { F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) } ;
consider f being Function such that
A3: dom f = [:(F3() /\ F1()),(F4() /\ F2()):] and
A4: for y being object st y in [:(F3() /\ F1()),(F4() /\ F2()):] holds
f . y = H1(y) from FUNCT_1:sch 3();
 A5: dom f = [:F3(),F4():] /\ [:F1(),F2():] by A3, ZFMISC_1:100;
{ F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) } = f .: [:F3(),F4():]
proof
thus { F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) } c= f .: [:F3(),F4():] :: according to XBOOLE_0:def 10 :: thesis: f .: [:F3(),F4():] c= { F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) } or x in f .: [:F3(),F4():] )
assume x in { F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) } ; :: thesis: x in f .: [:F3(),F4():]
then consider u being Element of F1(), v being Element of F2() such that
A6: x = F5(u,v) and
A7: u in F3() and
A8: v in F4() ;
A9: [u,v] in [:F3(),F4():] 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) = F5(u,v) by A3, A4, A10, A11;
hence x in f .: [:F3(),F4():] 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 .: [:F3(),F4():] or x in { F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) } )
assume x in f .: [:F3(),F4():] ; :: thesis: x in { F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) }
then consider y being object such that
A12: y in dom f and
A13: y in [:F3(),F4():] and
A14: x = f . y by FUNCT_1:def 6;
reconsider y = y as Element of [:F1(),F2():] by A5, A12, XBOOLE_0:def 4;
A15: y = [(y `1),(y `2)] by MCART_1:21;
then A16: y `1 in F3() by A13, ZFMISC_1:87;
A17: y `2 in F4() by A13, A15, ZFMISC_1:87;
x = F5((y `1),(y `2)) by A3, A4, A12, A14;
hence x in { F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() ) } by A16, A17; :: thesis: verum
end;
hence { F5(u,v) where u is Element of F1(), v is Element of F2() : ( u in F3() & v in F4() ) } is finite by A1, A2; :: thesis: verum