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 S: A = {} ; :: thesis: (RealFuncAdd A) . f,((RealFuncExtMult A) . [(- 1),f]) = RealFuncZero A

thus (RealFuncAdd A) . f,((RealFuncExtMult A) . [(- 1),f]) = {} by S
.= RealFuncZero A by S ; :: 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;