theorem Th8:
for
x1,
x2,
x3,
x4 being
Variable 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) )