let D be non empty set ; :: thesis: for X, Y, Z, S being set
for f1, f2 being Function of [:X,Y,Z,S:],D st ( for x, y, z, s being set st x in X & y in Y & z in Z & s in S holds
f1 . [x,y,z,s] = f2 . [x,y,z,s] ) holds
f1 = f2
let X, Y, Z, S be set ; :: thesis: for f1, f2 being Function of [:X,Y,Z,S:],D st ( for x, y, z, s being set st x in X & y in Y & z in Z & s in S holds
f1 . [x,y,z,s] = f2 . [x,y,z,s] ) holds
f1 = f2
let f1, f2 be Function of [:X,Y,Z,S:],D; :: thesis: ( ( for x, y, z, s being set st x in X & y in Y & z in Z & s in S holds
f1 . [x,y,z,s] = f2 . [x,y,z,s] ) implies f1 = f2 )
assume A1: for x, y, z, s being set st x in X & y in Y & z in Z & s in S holds
f1 . [x,y,z,s] = f2 . [x,y,z,s] ; :: thesis: f1 = f2
for t being set st t in [:X,Y,Z,S:] holds
f1 . t = f2 . t

proof

let t be set ; :: thesis: ( t in [:X,Y,Z,S:] implies f1 . t = f2 . t )
assume t in [:X,Y,Z,S:] ; :: thesis: f1 . t = f2 . t
then ex x, y, z, s being set st
( x in X & y in Y & z in Z & s in S & t = [x,y,z,s] ) by MCART_1:83;
hence f1 . t = f2 . t by A1; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:18; :: thesis: verum