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

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