deffunc H_{1}( object ) -> object = F_{5}(($1 `1),($1 `2));

set M = { F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) } ;

consider f being Function such that

A3: dom f = [:(F_{3}() /\ F_{1}()),(F_{4}() /\ F_{2}()):]
and

A4: for y being object st y in [:(F_{3}() /\ F_{1}()),(F_{4}() /\ F_{2}()):] holds

f . y = H_{1}(y)
from FUNCT_1:sch 3();

A5: dom f = [:F_{3}(),F_{4}():] /\ [:F_{1}(),F_{2}():]
by A3, ZFMISC_1:100;

{ F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) } = f .: [:F_{3}(),F_{4}():]
_{5}(u,v) where u is Element of F_{1}(), v is Element of F_{2}() : ( u in F_{3}() & v in F_{4}() ) } is finite
by A1, A2; :: thesis: verum

set M = { F

consider f being Function such that

A3: dom f = [:(F

A4: for y being object st y in [:(F

f . y = H

A5: dom f = [:F

{ F

proof

hence
{ F
thus
{ F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) } c= f .: [:F_{3}(),F_{4}():]
:: according to XBOOLE_0:def 10 :: thesis: f .: [:F_{3}(),F_{4}():] c= { F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) } _{3}(),F_{4}():] or x in { F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) } )

assume x in f .: [:F_{3}(),F_{4}():]
; :: thesis: x in { F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) }

then consider y being object such that

A12: y in dom f and

A13: y in [:F_{3}(),F_{4}():]
and

A14: x = f . y by FUNCT_1:def 6;

reconsider y = y as Element of [:F_{1}(),F_{2}():] by A5, A12, XBOOLE_0:def 4;

A15: y = [(y `1),(y `2)] by MCART_1:21;

then A16: y `1 in F_{3}()
by A13, ZFMISC_1:87;

A17: y `2 in F_{4}()
by A13, A15, ZFMISC_1:87;

x = F_{5}((y `1),(y `2))
by A3, A4, A12, A14;

hence x in { F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) }
by A16, A17; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: [:F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) } or x in f .: [:F_{3}(),F_{4}():] )

assume x in { F_{5}(u9,v9) where u9 is Element of F_{1}(), v9 is Element of F_{2}() : ( u9 in F_{3}() & v9 in F_{4}() ) }
; :: thesis: x in f .: [:F_{3}(),F_{4}():]

then consider u being Element of F_{1}(), v being Element of F_{2}() such that

A6: x = F_{5}(u,v)
and

A7: u in F_{3}()
and

A8: v in F_{4}()
;

A9: [u,v] in [:F_{3}(),F_{4}():]
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_{5}(u,v)
by A3, A4, A10, A11;

hence x in f .: [:F_{3}(),F_{4}():]
by A6, A9, A10, FUNCT_1:def 6; :: thesis: verum

end;assume x in { F

then consider u being Element of F

A6: x = F

A7: u in F

A8: v in F

A9: [u,v] in [:F

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

hence x in f .: [:F

assume x in f .: [:F

then consider y being object such that

A12: y in dom f and

A13: y in [:F

A14: x = f . y by FUNCT_1:def 6;

reconsider y = y as Element of [:F

A15: y = [(y `1),(y `2)] by MCART_1:21;

then A16: y `1 in F

A17: y `2 in F

x = F

hence x in { F