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