let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom [:f,g:] or not y in dom [:f,g:] or not [:f,g:] . x = [:f,g:] . y or x = y )
assume that
A1: x in dom [:f,g:] and
A2: y in dom [:f,g:] and
A3: [:f,g:] . x = [:f,g:] . y ; :: thesis: x = y
A4: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 8;
then consider x1, x2 being object such that
A5: x1 in dom f and
A6: x2 in dom g and
A7: x = [x1,x2] by A1, ZFMISC_1:def 2;
A8: [:f,g:] . (x1,x2) = [(f . x1),(g . x2)] by A5, A6, FUNCT_3:def 8;
consider y1, y2 being object such that
A9: y1 in dom f and
A10: y2 in dom g and
A11: y = [y1,y2] by A2, A4, ZFMISC_1:def 2;
A12: [:f,g:] . (y1,y2) = [(f . y1),(g . y2)] by A9, A10, FUNCT_3:def 8;
then f . x1 = f . y1 by A3, A7, A11, A8, XTUPLE_0:1;
then A13: x1 = y1 by A5, A9, FUNCT_1:def 4;
g . x2 = g . y2 by A3, A7, A11, A8, A12, XTUPLE_0:1;
hence x = y by A6, A7, A10, A11, A13, FUNCT_1:def 4; :: thesis: verum