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

then (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- jj),f])) = {}
.= RealFuncZero A by A1 ;
hence (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A ; :: 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 :: thesis: for x being Element of A holds ((RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- jj),f]))) . x = (RealFuncZero A) . x

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

end;

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

end;

end;