let n be Element of NAT ; for f1, f2 being PartFunc of REAL ,(REAL n)
for i being Element of NAT holds
( (proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2) & (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2) )
let f1, f2 be PartFunc of REAL ,(REAL n); for i being Element of NAT holds
( (proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2) & (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2) )
let i be Element of NAT ; ( (proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2) & (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2) )
A1:
dom (proj i,n) = REAL n
by FUNCT_2:def 1;
then
rng f1 c= dom (proj i,n)
;
then A2:
dom ((proj i,n) * f1) = dom f1
by RELAT_1:46;
A3:
rng (f1 + f2) c= dom (proj i,n)
by A1;
then A4:
dom ((proj i,n) * (f1 + f2)) = dom (f1 + f2)
by RELAT_1:46;
rng f2 c= dom (proj i,n)
by A1;
then A5:
dom ((proj i,n) * f2) = dom f2
by RELAT_1:46;
A6:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by Def9;
A7:
for z being Element of REAL st z in dom ((proj i,n) * (f1 + f2)) holds
((proj i,n) * (f1 + f2)) . z = (((proj i,n) * f1) + ((proj i,n) * f2)) . z
proof
let z be
Element of
REAL ;
( z in dom ((proj i,n) * (f1 + f2)) implies ((proj i,n) * (f1 + f2)) . z = (((proj i,n) * f1) + ((proj i,n) * f2)) . z )
reconsider f1z =
f1 /. z as
Element of
n -tuples_on REAL ;
reconsider f2z =
f2 /. z as
Element of
n -tuples_on REAL ;
assume A8:
z in dom ((proj i,n) * (f1 + f2))
;
((proj i,n) * (f1 + f2)) . z = (((proj i,n) * f1) + ((proj i,n) * f2)) . z
then A9:
z in dom (f1 + f2)
by A3, RELAT_1:46;
then A10:
z in (dom f1) /\ (dom f2)
by Def9;
then
z in dom f1
by XBOOLE_0:def 4;
then A11:
f1 . z = f1z
by PARTFUN1:def 8;
(proj i,n) . ((f1 + f2) . z) = (proj i,n) . ((f1 + f2) /. z)
by A9, PARTFUN1:def 8;
then
(proj i,n) . ((f1 + f2) . z) = (proj i,n) . ((f1 /. z) + (f2 /. z))
by A9, Def9;
then
(proj i,n) . ((f1 + f2) . z) = ((f1 /. z) + (f2 /. z)) . i
by PDIFF_1:def 1;
then A12:
(proj i,n) . ((f1 + f2) . z) = (f1z . i) + (f2z . i)
by RVSUM_1:27;
z in dom f2
by A10, XBOOLE_0:def 4;
then A13:
f2 . z = f2z
by PARTFUN1:def 8;
A14:
z in (dom ((proj i,n) * f1)) /\ (dom ((proj i,n) * f2))
by A2, A5, A4, A8, Def9;
then
z in dom ((proj i,n) * f1)
by XBOOLE_0:def 4;
then
((proj i,n) * f1) . z = (proj i,n) . (f1 . z)
by FUNCT_1:22;
then A15:
((proj i,n) * f1) . z = f1z . i
by A11, PDIFF_1:def 1;
z in dom ((proj i,n) * f2)
by A14, XBOOLE_0:def 4;
then
((proj i,n) * f2) . z = (proj i,n) . (f2 . z)
by FUNCT_1:22;
then A16:
((proj i,n) * f2) . z = f2z . i
by A13, PDIFF_1:def 1;
z in dom (((proj i,n) * f1) + ((proj i,n) * f2))
by A6, A2, A5, A4, A8, VALUED_1:def 1;
then
(((proj i,n) * f1) + ((proj i,n) * f2)) . z = (f1z . i) + (f2z . i)
by A15, A16, VALUED_1:def 1;
hence
((proj i,n) * (f1 + f2)) . z = (((proj i,n) * f1) + ((proj i,n) * f2)) . z
by A8, A12, FUNCT_1:22;
verum
end;
dom ((proj i,n) * (f1 + f2)) = dom (((proj i,n) * f1) + ((proj i,n) * f2))
by A6, A2, A5, A4, VALUED_1:def 1;
hence
(proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2)
by A7, PARTFUN1:34; (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2)
A17:
rng (f1 - f2) c= dom (proj i,n)
by A1;
then A18:
dom ((proj i,n) * (f1 - f2)) = dom (f1 - f2)
by RELAT_1:46;
A19:
dom (f1 - f2) = (dom f1) /\ (dom f2)
by Def10;
then A20:
dom ((proj i,n) * (f1 - f2)) = dom (((proj i,n) * f1) - ((proj i,n) * f2))
by A2, A5, A18, VALUED_1:12;
for z being Element of REAL st z in dom ((proj i,n) * (f1 - f2)) holds
((proj i,n) * (f1 - f2)) . z = (((proj i,n) * f1) - ((proj i,n) * f2)) . z
proof
let z be
Element of
REAL ;
( z in dom ((proj i,n) * (f1 - f2)) implies ((proj i,n) * (f1 - f2)) . z = (((proj i,n) * f1) - ((proj i,n) * f2)) . z )
reconsider f1z =
f1 /. z as
Element of
n -tuples_on REAL ;
reconsider f2z =
f2 /. z as
Element of
n -tuples_on REAL ;
assume A21:
z in dom ((proj i,n) * (f1 - f2))
;
((proj i,n) * (f1 - f2)) . z = (((proj i,n) * f1) - ((proj i,n) * f2)) . z
then A22:
z in dom (f1 - f2)
by A17, RELAT_1:46;
then A23:
z in (dom f1) /\ (dom f2)
by Def10;
then
z in dom f1
by XBOOLE_0:def 4;
then A24:
f1 . z = f1z
by PARTFUN1:def 8;
z in dom f2
by A23, XBOOLE_0:def 4;
then A25:
f2 . z = f2z
by PARTFUN1:def 8;
z in dom ((proj i,n) * f2)
by A5, A19, A18, A21, XBOOLE_0:def 4;
then
((proj i,n) * f2) . z = (proj i,n) . (f2 . z)
by FUNCT_1:22;
then A26:
((proj i,n) * f2) . z = f2z . i
by A25, PDIFF_1:def 1;
(proj i,n) . ((f1 - f2) . z) = (proj i,n) . ((f1 - f2) /. z)
by A22, PARTFUN1:def 8;
then
(proj i,n) . ((f1 - f2) . z) = (proj i,n) . ((f1 /. z) - (f2 /. z))
by A22, Def10;
then
(proj i,n) . ((f1 - f2) . z) = ((f1 /. z) - (f2 /. z)) . i
by PDIFF_1:def 1;
then A27:
(proj i,n) . ((f1 - f2) . z) = (f1z . i) - (f2z . i)
by RVSUM_1:48;
z in dom ((proj i,n) * f1)
by A2, A19, A18, A21, XBOOLE_0:def 4;
then
((proj i,n) * f1) . z = (proj i,n) . (f1 . z)
by FUNCT_1:22;
then A28:
((proj i,n) * f1) . z = f1z . i
by A24, PDIFF_1:def 1;
(((proj i,n) * f1) - ((proj i,n) * f2)) . z = (((proj i,n) * f1) . z) - (((proj i,n) * f2) . z)
by A20, A21, VALUED_1:13;
hence
((proj i,n) * (f1 - f2)) . z = (((proj i,n) * f1) - ((proj i,n) * f2)) . z
by A21, A27, A28, A26, FUNCT_1:22;
verum
end;
hence
(proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2)
by A20, PARTFUN1:34; verum