let x, y be object ; FUNCT_1:def 4 ( 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
; 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; verum