let A, B be RelStr ; :: thesis: for C being non empty RelStr
for f, g being Function of [:A,B:],C st ( for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ) holds
f = g
let C be non empty RelStr ; :: thesis: for f, g being Function of [:A,B:],C st ( for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ) holds
f = g
let f, g be Function of [:A,B:],C; :: thesis: ( ( for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ) implies f = g )
assume for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ; :: thesis: f = g
then A1: for x, y being set st x in the carrier of A & y in the carrier of B holds
f . (x,y) = g . (x,y) ;
the carrier of [:A,B:] = [: the carrier of A, the carrier of B:] by Def2;
hence f = g by A1, BINOP_1:1; :: thesis: verum