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

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:9;
consider b2 being Element of B, c2 being Element of C such that
A3: g . a = [b2,c2] by DOMAIN_1:9;
A4: ( (pr1 B,C) . b1,c1 = b1 & (pr1 B,C) . b2,c2 = b2 & (pr2 B,C) . b1,c1 = c1 & (pr2 B,C) . b2,c2 = c2 ) by FUNCT_3:def 5, FUNCT_3:def 6;
( (pr1 B,C) . (f . a) = ((pr1 B,C) * f) . a & (pr2 B,C) . (f . a) = ((pr2 B,C) * f) . a & (pr1 B,C) . (g . a) = ((pr1 B,C) * g) . a & (pr2 B,C) . (g . a) = ((pr2 B,C) * g) . a ) by FUNCT_2:21;
hence f . a = g . a by A1, A2, A3, A4; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum