let x1, x2, x3, x4 be Variable; :: thesis: for M being non empty set
for m1, m2, m, m3, m4 being Element of M
for v being Function of VAR ,M holds
( ((v / x1,m1) / x2,m2) / x1,m = (v / x2,m2) / x1,m & (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = ((v / x2,m2) / x3,m3) / x1,m & ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m )
let M be non empty set ; :: thesis: for m1, m2, m, m3, m4 being Element of M
for v being Function of VAR ,M holds
( ((v / x1,m1) / x2,m2) / x1,m = (v / x2,m2) / x1,m & (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = ((v / x2,m2) / x3,m3) / x1,m & ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m )
let m1, m2, m, m3, m4 be Element of M; :: thesis: for v being Function of VAR ,M holds
( ((v / x1,m1) / x2,m2) / x1,m = (v / x2,m2) / x1,m & (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = ((v / x2,m2) / x3,m3) / x1,m & ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m )
let v be Function of VAR ,M; :: thesis: ( ((v / x1,m1) / x2,m2) / x1,m = (v / x2,m2) / x1,m & (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = ((v / x2,m2) / x3,m3) / x1,m & ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m )
A1: ( ((v / x1,m1) / x2,m2) / x1,m = ((v / x2,m2) / x1,m1) / x1,m or x1 = x2 ) by FUNCT_7:35;
hence ((v / x1,m1) / x2,m2) / x1,m = (v / x2,m2) / x1,m by FUNCT_7:36; :: thesis: ( (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = ((v / x2,m2) / x3,m3) / x1,m & ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m )
( x1 = x3 or x1 <> x3 ) ;
then A2: ( ( (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = (((v / x1,m1) / x2,m2) / x1,m) / x3,m3 & ((v / x2,m2) / x3,m3) / x1,m = ((v / x2,m2) / x1,m) / x3,m3 ) or ( (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = ((v / x1,m1) / x2,m2) / x1,m & ((v / x2,m2) / x3,m3) / x1,m = (v / x2,m2) / x1,m ) ) by FUNCT_7:35, FUNCT_7:36;
hence (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = ((v / x2,m2) / x3,m3) / x1,m by A1, FUNCT_7:36; :: thesis: ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m
( x1 = x4 or x1 <> x4 ) ;
then ( ( ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = ((((v / x1,m1) / x2,m2) / x3,m3) / x1,m) / x4,m4 & (((v / x2,m2) / x3,m3) / x1,m) / x4,m4 = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m ) or ( ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x1,m1) / x2,m2) / x3,m3) / x1,m & (((v / x2,m2) / x3,m3) / x4,m4) / x1,m = ((v / x2,m2) / x3,m3) / x1,m ) ) by FUNCT_7:35, FUNCT_7:36;
hence ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m by A1, A2, FUNCT_7:36; :: thesis: verum