let A be set ; :: thesis: for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A
let f be Element of Funcs (A,REAL); :: thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A

per cases ( A = {} or A <> {} ) ;

suppose A1: A = {} ; :: thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A

hence (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = {}
.= RealFuncZero A by A1 ;
:: thesis: verum

end;

suppose A <> {} ; :: thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A

then reconsider A = A as non empty set ;
reconsider f = f as Element of Funcs (A,REAL) ;

now

let x be Element of A; :: thesis: ((RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f]))) . x = (RealFuncZero A) . x
set y = f . x;
thus ((RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f]))) . x = (f . x) + (((RealFuncExtMult A) . [(- 1),f]) . x) by Th10
.= (f . x) + ((- 1) * (f . x)) by Th15
.= (RealFuncZero A) . x by FUNCOP_1:13 ; :: thesis: verum

end;

hence (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A by FUNCT_2:113; :: thesis: verum

end;

end;