let A be non empty set ; for f, g, h being Element of Funcs (A,REAL) holds (minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (g,h)))
let f, g, h be Element of Funcs (A,REAL); (minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (g,h)))
now for x being Element of A holds ((minfuncreal A) . (((minfuncreal A) . (f,g)),h)) . x = ((minfuncreal A) . (f,((minfuncreal A) . (g,h)))) . xlet x be
Element of
A;
((minfuncreal A) . (((minfuncreal A) . (f,g)),h)) . x = ((minfuncreal A) . (f,((minfuncreal A) . (g,h)))) . xA1:
x in dom (minreal .: (f,g))
by Lm6;
A2:
x in dom (minreal .: (g,h))
by Lm6;
A3:
x in dom (minreal .: ((minreal .: (f,g)),h))
by Lm6;
A4:
x in dom (minreal .: (f,(minreal .: (g,h))))
by Lm6;
thus ((minfuncreal A) . (((minfuncreal A) . (f,g)),h)) . x =
((minfuncreal A) . ((minreal .: (f,g)),h)) . x
by Def5
.=
(minreal .: ((minreal .: (f,g)),h)) . x
by Def5
.=
minreal . (
((minreal .: (f,g)) . x),
(h . x))
by A3, FUNCOP_1:22
.=
minreal . (
(minreal . ((f . x),(g . x))),
(h . x))
by A1, FUNCOP_1:22
.=
minreal . (
(f . x),
(minreal . ((g . x),(h . x))))
by Th4
.=
minreal . (
(f . x),
((minreal .: (g,h)) . x))
by A2, FUNCOP_1:22
.=
(minreal .: (f,(minreal .: (g,h)))) . x
by A4, FUNCOP_1:22
.=
((minfuncreal A) . (f,(minreal .: (g,h)))) . x
by Def5
.=
((minfuncreal A) . (f,((minfuncreal A) . (g,h)))) . x
by Def5
;
verum end;
hence
(minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (g,h)))
by FUNCT_2:63; verum