let x, y, z be Variable; :: thesis: for M being non empty set
for m1, m2, m3 being Element of M
for v being Function of VAR ,M st x <> y & y <> z & z <> x holds
( ((v / x,m1) / y,m2) / z,m3 = ((v / z,m3) / y,m2) / x,m1 & ((v / x,m1) / y,m2) / z,m3 = ((v / y,m2) / z,m3) / x,m1 )
let M be non empty set ; :: thesis: for m1, m2, m3 being Element of M
for v being Function of VAR ,M st x <> y & y <> z & z <> x holds
( ((v / x,m1) / y,m2) / z,m3 = ((v / z,m3) / y,m2) / x,m1 & ((v / x,m1) / y,m2) / z,m3 = ((v / y,m2) / z,m3) / x,m1 )
let m1, m2, m3 be Element of M; :: thesis: for v being Function of VAR ,M st x <> y & y <> z & z <> x holds
( ((v / x,m1) / y,m2) / z,m3 = ((v / z,m3) / y,m2) / x,m1 & ((v / x,m1) / y,m2) / z,m3 = ((v / y,m2) / z,m3) / x,m1 )
let v be Function of VAR ,M; :: thesis: ( x <> y & y <> z & z <> x implies ( ((v / x,m1) / y,m2) / z,m3 = ((v / z,m3) / y,m2) / x,m1 & ((v / x,m1) / y,m2) / z,m3 = ((v / y,m2) / z,m3) / x,m1 ) )
assume ( x <> y & y <> z & z <> x ) ; :: thesis: ( ((v / x,m1) / y,m2) / z,m3 = ((v / z,m3) / y,m2) / x,m1 & ((v / x,m1) / y,m2) / z,m3 = ((v / y,m2) / z,m3) / x,m1 )
then ( (v / x,m1) / y,m2 = (v / y,m2) / x,m1 & (v / z,m3) / y,m2 = (v / y,m2) / z,m3 & ((v / y,m2) / x,m1) / z,m3 = ((v / y,m2) / z,m3) / x,m1 ) by FUNCT_7:35;
hence ( ((v / x,m1) / y,m2) / z,m3 = ((v / z,m3) / y,m2) / x,m1 & ((v / x,m1) / y,m2) / z,m3 = ((v / y,m2) / z,m3) / x,m1 ) ; :: thesis: verum