let n, m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
let i be Element of NAT ; :: thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
let x be Point of (REAL-NS m); :: thesis: ( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
A1: dom (reproj i,x) = the carrier of (REAL-NS 1) by FUNCT_2:def 1;
A2: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def 1;
for s being Element of (REAL-NS 1) holds
( s in dom ((f1 + f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) )

proof

let s be Element of (REAL-NS 1); :: thesis: ( s in dom ((f1 + f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) )
( s in dom ((f1 + f2) * (reproj i,x)) iff (reproj i,x) . s in (dom f1) /\ (dom f2) ) by A2, A1, FUNCT_1:21;
then ( s in dom ((f1 + f2) * (reproj i,x)) iff ( (reproj i,x) . s in dom f1 & (reproj i,x) . s in dom f2 ) ) by XBOOLE_0:def 4;
then ( s in dom ((f1 + f2) * (reproj i,x)) iff ( s in dom (f1 * (reproj i,x)) & s in dom (f2 * (reproj i,x)) ) ) by A1, FUNCT_1:21;
then ( s in dom ((f1 + f2) * (reproj i,x)) iff s in (dom (f1 * (reproj i,x))) /\ (dom (f2 * (reproj i,x))) ) by XBOOLE_0:def 4;
hence ( s in dom ((f1 + f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) ) by VFUNCT_1:def 1; :: thesis: verum

end;

then for s being set holds
( s in dom ((f1 + f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) ) ;
then A3: dom ((f1 + f2) * (reproj i,x)) = dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) by TARSKI:2;
A4: for z being Element of (REAL-NS 1) st z in dom ((f1 + f2) * (reproj i,x)) holds
((f1 + f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) . z

proof

let z be Element of (REAL-NS 1); :: thesis: ( z in dom ((f1 + f2) * (reproj i,x)) implies ((f1 + f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) . z )
assume A5: z in dom ((f1 + f2) * (reproj i,x)) ; :: thesis: ((f1 + f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) . z
then A6: (reproj i,x) . z in dom (f1 + f2) by FUNCT_1:21;
A7: (reproj i,x) . z in (dom f1) /\ (dom f2) by A2, A5, FUNCT_1:21;
then A8: (reproj i,x) . z in dom f1 by XBOOLE_0:def 4;
then A9: z in dom (f1 * (reproj i,x)) by A1, FUNCT_1:21;
A10: (reproj i,x) . z in dom f2 by A7, XBOOLE_0:def 4;
then A11: z in dom (f2 * (reproj i,x)) by A1, FUNCT_1:21;
A12: f2 /. ((reproj i,x) . z) = f2 . ((reproj i,x) . z) by A10, PARTFUN1:def 8
.= (f2 * (reproj i,x)) . z by A11, FUNCT_1:22
.= (f2 * (reproj i,x)) /. z by A11, PARTFUN1:def 8 ;
A13: f1 /. ((reproj i,x) . z) = f1 . ((reproj i,x) . z) by A8, PARTFUN1:def 8
.= (f1 * (reproj i,x)) . z by A9, FUNCT_1:22
.= (f1 * (reproj i,x)) /. z by A9, PARTFUN1:def 8 ;
((f1 + f2) * (reproj i,x)) . z = (f1 + f2) . ((reproj i,x) . z) by A5, FUNCT_1:22
.= (f1 + f2) /. ((reproj i,x) . z) by A6, PARTFUN1:def 8
.= (f1 /. ((reproj i,x) . z)) + (f2 /. ((reproj i,x) . z)) by A6, VFUNCT_1:def 1
.= ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) /. z by A3, A5, A13, A12, VFUNCT_1:def 1 ;
hence ((f1 + f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) . z by A3, A5, PARTFUN1:def 8; :: thesis: verum

end;

A14: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def 2;
for s being Element of (REAL-NS 1) holds
( s in dom ((f1 - f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) )

proof

let s be Element of (REAL-NS 1); :: thesis: ( s in dom ((f1 - f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) )
( s in dom ((f1 - f2) * (reproj i,x)) iff (reproj i,x) . s in (dom f1) /\ (dom f2) ) by A14, A1, FUNCT_1:21;
then ( s in dom ((f1 - f2) * (reproj i,x)) iff ( (reproj i,x) . s in dom f1 & (reproj i,x) . s in dom f2 ) ) by XBOOLE_0:def 4;
then ( s in dom ((f1 - f2) * (reproj i,x)) iff ( s in dom (f1 * (reproj i,x)) & s in dom (f2 * (reproj i,x)) ) ) by A1, FUNCT_1:21;
then ( s in dom ((f1 - f2) * (reproj i,x)) iff s in (dom (f1 * (reproj i,x))) /\ (dom (f2 * (reproj i,x))) ) by XBOOLE_0:def 4;
hence ( s in dom ((f1 - f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) ) by VFUNCT_1:def 2; :: thesis: verum

end;

then for s being set holds
( s in dom ((f1 - f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) ) ;
then A15: dom ((f1 - f2) * (reproj i,x)) = dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) by TARSKI:2;
for z being Element of (REAL-NS 1) st z in dom ((f1 - f2) * (reproj i,x)) holds
((f1 - f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) . z

proof

let z be Element of (REAL-NS 1); :: thesis: ( z in dom ((f1 - f2) * (reproj i,x)) implies ((f1 - f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) . z )
assume A16: z in dom ((f1 - f2) * (reproj i,x)) ; :: thesis: ((f1 - f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) . z
then A17: (reproj i,x) . z in dom (f1 - f2) by FUNCT_1:21;
A18: (reproj i,x) . z in (dom f1) /\ (dom f2) by A14, A16, FUNCT_1:21;
then A19: (reproj i,x) . z in dom f1 by XBOOLE_0:def 4;
then A20: z in dom (f1 * (reproj i,x)) by A1, FUNCT_1:21;
A21: (reproj i,x) . z in dom f2 by A18, XBOOLE_0:def 4;
then A22: z in dom (f2 * (reproj i,x)) by A1, FUNCT_1:21;
A23: f2 /. ((reproj i,x) . z) = f2 . ((reproj i,x) . z) by A21, PARTFUN1:def 8
.= (f2 * (reproj i,x)) . z by A22, FUNCT_1:22
.= (f2 * (reproj i,x)) /. z by A22, PARTFUN1:def 8 ;
A24: f1 /. ((reproj i,x) . z) = f1 . ((reproj i,x) . z) by A19, PARTFUN1:def 8
.= (f1 * (reproj i,x)) . z by A20, FUNCT_1:22
.= (f1 * (reproj i,x)) /. z by A20, PARTFUN1:def 8 ;
thus ((f1 - f2) * (reproj i,x)) . z = (f1 - f2) . ((reproj i,x) . z) by A16, FUNCT_1:22
.= (f1 - f2) /. ((reproj i,x) . z) by A17, PARTFUN1:def 8
.= (f1 /. ((reproj i,x) . z)) - (f2 /. ((reproj i,x) . z)) by A17, VFUNCT_1:def 2
.= ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) /. z by A15, A16, A24, A23, VFUNCT_1:def 2
.= ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) . z by A15, A16, PARTFUN1:def 8 ; :: thesis: verum

end;

hence ( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) ) by A3, A15, A4, PARTFUN1:34; :: thesis: verum