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 ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & 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 )
then ( ((v / x1,m1) / x2,m2) / x3,m3 = ((v / x2,m2) / x3,m3) / x1,m1 & (((v / x2,m2) / x3,m3) / x1,m1) / x4,m4 = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m1 & (((v / x1,m1) / x2,m2) / x3,m3) / x4,m4 = (((v / x1,m1) / x3,m3) / x4,m4) / x2,m2 & (((v / x1,m1) / x3,m3) / x4,m4) / x2,m2 = (((v / x3,m3) / x4,m4) / x1,m1) / x2,m2 & ((v / x2,m2) / x3,m3) / x4,m4 = ((v / x4,m4) / x2,m2) / x3,m3 ) by Th7, FUNCT_7:35;
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 ) ; :: thesis: verum