let x be set ; :: according to PARTIT_2:def 2 :: thesis: ( not x in dom [:f,g:] or [:f,g:] . ([:f,g:] . x) = x )

set h = [:f,g:];

A1: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 8;

assume x in dom [:f,g:] ; :: thesis: [:f,g:] . ([:f,g:] . x) = x

then consider a, b being object such that

A2: a in dom f and

A3: b in dom g and

A4: x = [a,b] by A1, ZFMISC_1:def 2;

A5: ( f . (f . a) = a & g . (g . b) = b ) by A2, A3, PARTIT_2:def 2;

A6: ( dom f = A & dom g = B ) by FUNCT_2:52;

A7: ( f . a in rng f & g . b in rng g ) by A2, A3, FUNCT_1:def 3;

[:f,g:] . (a,b) = [(f . a),(g . b)] by A2, A3, FUNCT_3:def 8;

hence [:f,g:] . ([:f,g:] . x) = [:f,g:] . ((f . a),(g . b)) by A4

.= x by A4, A5, A6, A7, FUNCT_3:def 8 ;

:: thesis: verum

set h = [:f,g:];

A1: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 8;

assume x in dom [:f,g:] ; :: thesis: [:f,g:] . ([:f,g:] . x) = x

then consider a, b being object such that

A2: a in dom f and

A3: b in dom g and

A4: x = [a,b] by A1, ZFMISC_1:def 2;

A5: ( f . (f . a) = a & g . (g . b) = b ) by A2, A3, PARTIT_2:def 2;

A6: ( dom f = A & dom g = B ) by FUNCT_2:52;

A7: ( f . a in rng f & g . b in rng g ) by A2, A3, FUNCT_1:def 3;

[:f,g:] . (a,b) = [(f . a),(g . b)] by A2, A3, FUNCT_3:def 8;

hence [:f,g:] . ([:f,g:] . x) = [:f,g:] . ((f . a),(g . b)) by A4

.= x by A4, A5, A6, A7, FUNCT_3:def 8 ;

:: thesis: verum