let F, G be Function; :: thesis: ( F is one-to-one & G is one-to-one implies [:F,G:] is one-to-one )
assume that
A1: F is one-to-one and
A2: G is one-to-one ; :: thesis: [:F,G:] is one-to-one
let z1, z2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not z1 in proj1 [:F,G:] or not z2 in proj1 [:F,G:] or not [:F,G:] . z1 = [:F,G:] . z2 or z1 = z2 )
assume that
A3: z1 in dom [:F,G:] and
A4: z2 in dom [:F,G:] and
A5: [:F,G:] . z1 = [:F,G:] . z2 ; :: thesis: z1 = z2
A6: dom [:F,G:] = [:(dom F),(dom G):] by FUNCT_3:def 9;
then consider x1, y1 being set such that
A7: x1 in dom F and
A8: y1 in dom G and
A9: z1 = [x1,y1] by A3, ZFMISC_1:103;
A10: [:F,G:] . x1,y1 = [(F . x1),(G . y1)] by A7, A8, FUNCT_3:def 9;
consider x2, y2 being set such that
A11: x2 in dom F and
A12: y2 in dom G and
A13: z2 = [x2,y2] by A4, A6, ZFMISC_1:103;
A14: [:F,G:] . x2,y2 = [(F . x2),(G . y2)] by A11, A12, FUNCT_3:def 9;
then F . x1 = F . x2 by A5, A9, A13, A10, ZFMISC_1:33;
then A15: x1 = x2 by A1, A7, A11, FUNCT_1:def 8;
G . y1 = G . y2 by A5, A9, A13, A10, A14, ZFMISC_1:33;
hence z1 = z2 by A2, A8, A9, A12, A13, A15, FUNCT_1:def 8; :: thesis: verum