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