let A, B, C be non empty set ; :: thesis: for f, g being Function of A,[:B,C:] st (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g holds
f = g
let f, g be Function of A,[:B,C:]; :: thesis: ( (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g implies f = g )
assume A1: ( (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g ) ; :: thesis: f = g

now :: thesis: for a being Element of A holds f . a = g . a

let a be Element of A; :: thesis: f . a = g . a
consider b1 being Element of B, c1 being Element of C such that
A2: f . a = [b1,c1] by DOMAIN_1:1;
consider b2 being Element of B, c2 being Element of C such that
A3: g . a = [b2,c2] by DOMAIN_1:1;
A4: (pr1 (B,C)) . (g . a) = ((pr1 (B,C)) * g) . a by FUNCT_2:15;
A5: ( (pr1 (B,C)) . (f . a) = ((pr1 (B,C)) * f) . a & (pr2 (B,C)) . (f . a) = ((pr2 (B,C)) * f) . a ) by FUNCT_2:15;
A6: ( (pr2 (B,C)) . (b1,c1) = c1 & (pr2 (B,C)) . (b2,c2) = c2 ) by Def5;
( (pr1 (B,C)) . (b1,c1) = b1 & (pr1 (B,C)) . (b2,c2) = b2 ) by Def4;
hence f . a = g . a by A1, A2, A3, A6, A5, A4, FUNCT_2:15; :: thesis: verum

end;

hence f = g ; :: thesis: verum