let x be set ; PARTIT_2:def 2 ( 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:]
; [: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
;
verum