let n, m be Nat; :: thesis: for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let f1, f2 be Function of (REAL m),(REAL n); :: thesis: for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let g1, g2 be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); :: thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; :: thesis: f1 - f2 = g1 - g2
A2: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider g12 = g1 - g2 as Function of (REAL m),(REAL n) by LOPBAN_1:def 9;
( g1 is LinearOperator of (REAL-NS m),(REAL-NS n) & g2 is LinearOperator of (REAL-NS m),(REAL-NS n) ) by LOPBAN_1:def 9;
then ( dom g1 = REAL m & dom g2 = REAL m ) by A2, FUNCT_2:def 1;
then A3: (dom f1) /\ (dom f2) = dom g12 by A1, FUNCT_2:def 1;
A4: f1 <--> f2 = f1 - f2 by INTEGR15:def 10;
for c being object st c in dom g12 holds
g12 . c = (f1 . c) - (f2 . c) hence f1 - f2 = g1 - g2 by A3, A4, VALUED_2:def 46; :: thesis: verum