let A be non empty set ; for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,g) = (maxfuncreal A) . (g,f)
let f, g be Element of Funcs (A,REAL); (maxfuncreal A) . (f,g) = (maxfuncreal A) . (g,f)
now for x being Element of A holds ((maxfuncreal A) . (f,g)) . x = ((maxfuncreal A) . (g,f)) . xlet x be
Element of
A;
((maxfuncreal A) . (f,g)) . x = ((maxfuncreal A) . (g,f)) . xA1:
x in dom (maxreal .: (f,g))
by Lm6;
A2:
x in dom (maxreal .: (g,f))
by Lm6;
thus ((maxfuncreal A) . (f,g)) . x =
(maxreal .: (f,g)) . x
by Def4
.=
maxreal . (
(f . x),
(g . x))
by A1, FUNCOP_1:22
.=
maxreal . (
(g . x),
(f . x))
by Th1
.=
(maxreal .: (g,f)) . x
by A2, FUNCOP_1:22
.=
((maxfuncreal A) . (g,f)) . x
by Def4
;
verum end;
hence
(maxfuncreal A) . (f,g) = (maxfuncreal A) . (g,f)
by FUNCT_2:63; verum