let m, n be non zero Element of NAT ; :: thesis: for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Nat
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
si - ti = (Proj (i,n)) * (s - t)
let s, t be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); :: thesis: for i being Nat
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
si - ti = (Proj (i,n)) * (s - t)
let i be Nat; :: thesis: for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
si - ti = (Proj (i,n)) * (s - t)
let si, ti be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))); :: thesis: ( si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n implies si - ti = (Proj (i,n)) * (s - t) )
assume A1: ( si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n ) ; :: thesis: si - ti = (Proj (i,n)) * (s - t)
deffunc H₁( non zero Element of NAT , non zero Element of NAT ) -> L16() = R_NormSpace_of_BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2));
A2: the carrier of (REAL-NS m) = REAL m by REAL_NS1:def 4;
A3: Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) by Th6, A1;
A4: dom (si - ti) = REAL m

proof

si - ti is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
hence dom (si - ti) = REAL m by A2, FUNCT_2:def 1; :: thesis: verum

end;

A5: dom (si - ti) = dom ((Proj (i,n)) * (s - t))

proof

s - t is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;
then (Proj (i,n)) * (s - t) is LinearOperator of (REAL-NS m),(REAL-NS 1) by A3, LOPBAN_2:1;
hence dom (si - ti) = dom ((Proj (i,n)) * (s - t)) by A4, A2, FUNCT_2:def 1; :: thesis: verum

end;

A6: dom si = REAL m

proof

si is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
hence dom si = REAL m by A2, FUNCT_2:def 1; :: thesis: verum

end;

A7: dom ti = REAL m

proof

ti is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
hence dom ti = REAL m by A2, FUNCT_2:def 1; :: thesis: verum

end;

A8: for x being Point of (REAL-NS m) holds (si - ti) . x = ((Proj (i,n)) * (s - t)) . x

proof

let x be Point of (REAL-NS m); :: thesis: (si - ti) . x = ((Proj (i,n)) * (s - t)) . x
reconsider x = x as Element of REAL m by REAL_NS1:def 4;
reconsider y = x as Point of (REAL-NS m) ;
((Proj (i,n)) * (s - t)) . x = (Proj (i,n)) . ((s - t) . x) by A4, A5, FUNCT_1:12
.= (Proj (i,n)) . ((s . y) - (t . y)) by LOPBAN_1:40
.= ((Proj (i,n)) . (s . y)) - ((Proj (i,n)) . (t . y)) by Th11
.= (si . y) - ((Proj (i,n)) . (t . y)) by A1, A6, FUNCT_1:12
.= (si . y) - (ti . y) by A1, A7, FUNCT_1:12
.= (si - ti) . x by LOPBAN_1:40 ;
hence (si - ti) . x = ((Proj (i,n)) * (s - t)) . x ; :: thesis: verum

end;

for x being object st x in dom (si - ti) holds
(si - ti) . x = ((Proj (i,n)) * (s - t)) . x

proof

let x be object ; :: thesis: ( x in dom (si - ti) implies (si - ti) . x = ((Proj (i,n)) * (s - t)) . x )
assume A9: x in dom (si - ti) ; :: thesis: (si - ti) . x = ((Proj (i,n)) * (s - t)) . x
reconsider x = x as Point of (REAL-NS m) by A9, A4, REAL_NS1:def 4;
(si - ti) . x = ((Proj (i,n)) * (s - t)) . x by A8;
hence (si - ti) . x = ((Proj (i,n)) * (s - t)) . x ; :: thesis: verum

end;

hence si - ti = (Proj (i,n)) * (s - t) by A5, FUNCT_1:2; :: thesis: verum