let D be non empty set ; :: thesis: for X, Y, Z being set
for f1, f2 being Function of [:X,Y,Z:],D st ( for x, y, z being object st x in X & y in Y & z in Z holds
f1 . [x,y,z] = f2 . [x,y,z] ) holds
f1 = f2
let X, Y, Z be set ; :: thesis: for f1, f2 being Function of [:X,Y,Z:],D st ( for x, y, z being object st x in X & y in Y & z in Z holds
f1 . [x,y,z] = f2 . [x,y,z] ) holds
f1 = f2
let f1, f2 be Function of [:X,Y,Z:],D; :: thesis: ( ( for x, y, z being object st x in X & y in Y & z in Z holds
f1 . [x,y,z] = f2 . [x,y,z] ) implies f1 = f2 )
assume A1: for x, y, z being object st x in X & y in Y & z in Z holds
f1 . [x,y,z] = f2 . [x,y,z] ; :: thesis: f1 = f2
for t being object st t in [:X,Y,Z:] holds
f1 . t = f2 . t
proof
let t be object ; :: thesis: ( t in [:X,Y,Z:] implies f1 . t = f2 . t )
assume t in [:X,Y,Z:] ; :: thesis: f1 . t = f2 . t
then ex x, y, z being object st
( x in X & y in Y & z in Z & t = [x,y,z] ) by MCART_1:68;
hence f1 . t = f2 . t by A1; :: thesis: verum
end;
hence f1 = f2 by FUNCT_2:12; :: thesis: verum