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 )
set F = Funcs ( the carrier of T,REAL);
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 )
ex map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD

proof

reconsider map0 = the carrier of T --> (In (0,REAL)) as RealMap of T ;
reconsider map09 = map0 as Element of Funcs ( the carrier of T,REAL) by FUNCT_2:8;
take map09 ; :: thesis: map09 is_a_unity_wrt ADD

now :: thesis: for f being Element of Funcs ( the carrier of T,REAL) holds
( ADD . (map0,f) = f & ADD . (f,map0) = f )

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

now :: thesis: for x being Element of T holds (f + map09) . x = f . x

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

end;

then f + map09 = f by FUNCT_2:63;
hence ( ADD . (map0,f) = f & ADD . (f,map0) = f ) by A1; :: thesis: verum

end;

hence map09 is_a_unity_wrt ADD by BINOP_1:3; :: thesis: verum

end;

hence ADD is having_a_unity by SETWISEO:def 2; :: thesis: ( ADD is commutative & ADD is associative )
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 2 :: thesis: ADD . (f1,f2) = ADD . (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 3 :: 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:66;
A2: ADD12 + f3 = ADD . (ADD12,f3) by A1;

now :: thesis: for t being Element of T holds (f1 + (f2 + f3)) . t = ((f1 + f2) + f3) . t

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;

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

end;