let D be non empty set ; 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 ; 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; ( ( 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]
; f1 = f2
for t being object st t in [:X,Y,Z:] holds
f1 . t = f2 . t
hence
f1 = f2
by FUNCT_2:12; verum