let x1, x2, x3, x4 be Variable; :: thesis: for M being non empty set
for m1, m2, m3, m4 being Element of M
for v being Function of VAR,M st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
( (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x4,m4)) / (x2,m2)) / (x3,m3)) / (x1,m1) )
let M be non empty set ; :: thesis: for m1, m2, m3, m4 being Element of M
for v being Function of VAR,M st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
( (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x4,m4)) / (x2,m2)) / (x3,m3)) / (x1,m1) )
let m1, m2, m3, m4 be Element of M; :: thesis: for v being Function of VAR,M st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
( (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x4,m4)) / (x2,m2)) / (x3,m3)) / (x1,m1) )
let v be Function of VAR,M; :: thesis: ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies ( (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x4,m4)) / (x2,m2)) / (x3,m3)) / (x1,m1) ) )
assume that
A1: x1 <> x2 and
A2: x1 <> x3 and
A3: x1 <> x4 and
A4: x2 <> x3 and
A5: x2 <> x4 and
A6: x3 <> x4 ; :: thesis: ( (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x4,m4)) / (x2,m2)) / (x3,m3)) / (x1,m1) )
A7: (((v / (x1,m1)) / (x3,m3)) / (x4,m4)) / (x2,m2) = (((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2) by A2, A3, A6, Th6;
A8: (((v / (x2,m2)) / (x3,m3)) / (x1,m1)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1) by A3, FUNCT_7:33;
((v / (x1,m1)) / (x2,m2)) / (x3,m3) = ((v / (x2,m2)) / (x3,m3)) / (x1,m1) by A1, A2, A4, Th6;
hence ( (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2) & (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4) = (((v / (x4,m4)) / (x2,m2)) / (x3,m3)) / (x1,m1) ) by A4, A5, A6, A8, A7, Th6; :: thesis: verum