let x1, x2, x3, x4 be Variable; :: thesis: for M being non empty set
for m, m1, m2, 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 m, m1, m2, 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, m1, m2, 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:33;
hence ((v / (x1,m1)) / (x2,m2)) / (x1,m) = (v / (x2,m2)) / (x1,m) by FUNCT_7:34; :: 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:33, FUNCT_7:34;
hence (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m) = ((v / (x2,m2)) / (x3,m3)) / (x1,m) by A1, FUNCT_7:34; :: 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:33, FUNCT_7:34;
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:34; :: thesis: verum