let T be non empty TopSpace; :: thesis: for ADD being BinOp of (Funcs the carrier of T,REAL ) st ( for f1, f2 being RealMap of T holds ADD . f1,f2 = f1 + f2 ) holds
( ADD is having_a_unity & ADD is commutative & ADD is associative )
let ADD be BinOp of (Funcs the carrier of T,REAL ); :: thesis: ( ( for f1, f2 being RealMap of T holds ADD . f1,f2 = f1 + f2 ) implies ( ADD is having_a_unity & ADD is commutative & ADD is associative ) )
assume A1: for f1, f2 being RealMap of T holds ADD . f1,f2 = f1 + f2 ; :: thesis: ( ADD is having_a_unity & ADD is commutative & ADD is associative )
set F = Funcs the carrier of T,REAL ;
thus ADD is having_a_unity :: thesis: ( ADD is commutative & ADD is associative )

proof

ex map' being Element of Funcs the carrier of T,REAL st map' is_a_unity_wrt ADD

proof

reconsider map0 = the carrier of T --> 0 as RealMap of T by FUNCOP_1:57;
reconsider map0' = map0 as Element of Funcs the carrier of T,REAL by FUNCT_2:11;
take map0' ; :: thesis: map0' is_a_unity_wrt ADD

now

let f be Element of Funcs the carrier of T,REAL ; :: thesis: ( ADD . map0,f = f & ADD . f,map0 = f )
A2: ADD . map0',f = f

proof

now

let x be Element of T; :: thesis: (map0' + f) . x = f . x
(map0' + f) . x = (map0' . x) + (f . x) by Def7;
then (map0' + f) . x = 0 + (f . x) by FUNCOP_1:13;
hence (map0' + f) . x = f . x ; :: thesis: verum

end;

then map0' + f = f by FUNCT_2:113;
hence ADD . map0',f = f by A1; :: thesis: verum

end;

ADD . f,map0' = f

proof

now

let x be Element of T; :: thesis: (f + map0') . x = f . x
(f + map0') . x = (f . x) + (map0' . x) by Def7;
then (f + map0') . x = (f . x) + 0 by FUNCOP_1:13;
hence (f + map0') . x = f . x ; :: thesis: verum

end;

then f + map0' = f by FUNCT_2:113;
hence ADD . f,map0' = f by A1; :: thesis: verum

end;

hence ( ADD . map0,f = f & ADD . f,map0 = f ) by A2; :: thesis: verum

end;

hence map0' is_a_unity_wrt ADD by BINOP_1:11; :: thesis: verum

end;

hence ADD is having_a_unity by SETWISEO:def 2; :: thesis: verum

end;

thus ADD is commutative :: thesis: ADD is associative

proof

let f1, f2 be Element of Funcs the carrier of T,REAL ; :: according to BINOP_1:def 13 :: thesis: ADD . f1,f2 = ADD . f2,f1
( f1 + f2 = f2 + f1 & ADD . f1,f2 = f1 + f2 ) by A1;
hence ADD . f1,f2 = ADD . f2,f1 by A1; :: thesis: verum

end;

thus ADD is associative :: thesis: verum

proof

let f1, f2, f3 be Element of Funcs the carrier of T,REAL ; :: according to BINOP_1:def 14 :: thesis: ADD . f1,(ADD . f2,f3) = ADD . (ADD . f1,f2),f3
reconsider ADD12 = ADD . f1,f2, ADD23 = ADD . f2,f3 as RealMap of T by FUNCT_2:121;
A3: f1 + (f2 + f3) = (f1 + f2) + f3

proof

now

let t be Element of T; :: thesis: (f1 + (f2 + f3)) . t = ((f1 + f2) + f3) . t
( (f1 + (f2 + f3)) . t = (f1 . t) + ((f2 + f3) . t) & (f2 + f3) . t = (f2 . t) + (f3 . t) ) by Def7;
then (f1 + (f2 + f3)) . t = ((f1 . t) + (f2 . t)) + (f3 . t) ;
then (f1 + (f2 + f3)) . t = ((f1 + f2) . t) + (f3 . t) by Def7;
hence (f1 + (f2 + f3)) . t = ((f1 + f2) + f3) . t by Def7; :: thesis: verum

end;

hence f1 + (f2 + f3) = (f1 + f2) + f3 by FUNCT_2:113; :: thesis: verum

end;

( f1 + (f2 + f3) = f1 + ADD23 & (f1 + f2) + f3 = ADD12 + f3 ) by A1;
then ( f1 + ADD23 = ADD12 + f3 & ADD12 + f3 = ADD . ADD12,f3 ) by A1, A3;
hence ADD . f1,(ADD . f2,f3) = ADD . (ADD . f1,f2),f3 by A1; :: thesis: verum

end;