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:33;
(v / (x,m1)) / (y,m2) = (v / (y,m2)) / (x,m1) by A1, FUNCT_7:33;
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:33; :: thesis: verum