let X, Y, Z, W be set ; :: thesis: ( Z <> {} & W <> {} implies for f being Function of [:X,Y:],Z
for g being Function of [:X,Y:],W st ( for a being Element of X
for b being Element of Y holds f . (a,b) = g . (a,b) ) holds
f = g )
assume A0: ( Z <> {} & W <> {} ) ; :: thesis: for f being Function of [:X,Y:],Z
for g being Function of [:X,Y:],W st ( for a being Element of X
for b being Element of Y holds f . (a,b) = g . (a,b) ) holds
f = g
let f be Function of [:X,Y:],Z; :: thesis: for g being Function of [:X,Y:],W st ( for a being Element of X
for b being Element of Y holds f . (a,b) = g . (a,b) ) holds
f = g
let g be Function of [:X,Y:],W; :: thesis: ( ( for a being Element of X
for b being Element of Y holds f . (a,b) = g . (a,b) ) implies f = g )
assume A1: for a being Element of X
for b being Element of Y holds f . (a,b) = g . (a,b) ; :: thesis: f = g
A2: ( dom f = [:X,Y:] & dom g = [:X,Y:] ) by FUNCT_2:def 1, A0;
for x, y being object st x in X & y in Y holds
f . (x,y) = g . (x,y) by A1;
hence f = g by A2, FUNCT_3:6; :: thesis: verum