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 that
A1: x <> y and
A2: y <> z and
A3: 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 )
A4: (v / z,m3) / y,m2 = (v / y,m2) / z,m3 by A2, FUNCT_7:35;
(v / x,m1) / y,m2 = (v / y,m2) / x,m1 by A1, 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 ) by A3, A4, FUNCT_7:35; :: thesis: verum