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

thus ADD is commutative :: thesis: ADD is associative

( 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

hence
ADD is having_a_unity
by SETWISEO:def 2; :: thesis: ( ADD is commutative & ADD is associative )
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

end;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 )

hence
map09 is_a_unity_wrt ADD
by BINOP_1:3; :: thesis: verum( 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 )

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

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

then
f + map09 = f
by FUNCT_2:63;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;(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

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

thus ADD is commutative :: thesis: ADD is associative

proof

thus
ADD is associative
:: thesis: verum
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;ADD . (f1,f2) = f1 + f2 by A1;

hence ADD . (f1,f2) = ADD . (f2,f1) by A1; :: 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;

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;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

then A3:
f1 + (f2 + f3) = (f1 + f2) + f3
by FUNCT_2:63;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;( (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

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