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 dom [:F,G:] or not z2 in dom [:F,G:] or not [:F,G:] . z1 = [:F,G:] . z2 or z1 = z2 )
assume A3: ( z1 in dom [:F,G:] & z2 in dom [:F,G:] & [:F,G:] . z1 = [:F,G:] . z2 ) ; :: thesis: z1 = z2
A4: dom [:F,G:] = [:(dom F),(dom G):] by FUNCT_3:def 9;
then consider x1, y1 being set such that
A5: ( x1 in dom F & y1 in dom G & z1 = [x1,y1] ) by A3, ZFMISC_1:103;
consider x2, y2 being set such that
A6: ( x2 in dom F & y2 in dom G & z2 = [x2,y2] ) by A3, A4, ZFMISC_1:103;
( [:F,G:] . x1,y1 = [(F . x1),(G . y1)] & [:F,G:] . x2,y2 = [(F . x2),(G . y2)] ) by A5, A6, FUNCT_3:def 9;
then ( F . x1 = F . x2 & G . y1 = G . y2 ) by A3, A5, A6, ZFMISC_1:33;
then ( x1 = x2 & y1 = y2 ) by A1, A2, A5, A6, FUNCT_1:def 8;
hence z1 = z2 by A5, A6; :: thesis: verum