let m, n be non zero Nat; for i being 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 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 f1, f2 be 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 x be Point of (REAL-NS m); ( (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);
( 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:11;
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:11;
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;
verum
end;
then
for s being object 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);
( 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)))
;
((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:11;
A7:
(reproj (i,x)) . z in (dom f1) /\ (dom f2)
by A2, A5, FUNCT_1:11;
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:11;
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:11;
A12:
f2 /. ((reproj (i,x)) . z) =
f2 . ((reproj (i,x)) . z)
by A10, PARTFUN1:def 6
.=
(f2 * (reproj (i,x))) . z
by A11, FUNCT_1:12
.=
(f2 * (reproj (i,x))) /. z
by A11, PARTFUN1:def 6
;
A13:
f1 /. ((reproj (i,x)) . z) =
f1 . ((reproj (i,x)) . z)
by A8, PARTFUN1:def 6
.=
(f1 * (reproj (i,x))) . z
by A9, FUNCT_1:12
.=
(f1 * (reproj (i,x))) /. z
by A9, PARTFUN1:def 6
;
((f1 + f2) * (reproj (i,x))) . z =
(f1 + f2) . ((reproj (i,x)) . z)
by A5, FUNCT_1:12
.=
(f1 + f2) /. ((reproj (i,x)) . z)
by A6, PARTFUN1:def 6
.=
(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 6;
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);
( 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:11;
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:11;
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;
verum
end;
then
for s being object 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);
( 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)))
;
((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:11;
A18:
(reproj (i,x)) . z in (dom f1) /\ (dom f2)
by A14, A16, FUNCT_1:11;
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:11;
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:11;
A23:
f2 /. ((reproj (i,x)) . z) =
f2 . ((reproj (i,x)) . z)
by A21, PARTFUN1:def 6
.=
(f2 * (reproj (i,x))) . z
by A22, FUNCT_1:12
.=
(f2 * (reproj (i,x))) /. z
by A22, PARTFUN1:def 6
;
A24:
f1 /. ((reproj (i,x)) . z) =
f1 . ((reproj (i,x)) . z)
by A19, PARTFUN1:def 6
.=
(f1 * (reproj (i,x))) . z
by A20, FUNCT_1:12
.=
(f1 * (reproj (i,x))) /. z
by A20, PARTFUN1:def 6
;
thus ((f1 - f2) * (reproj (i,x))) . z =
(f1 - f2) . ((reproj (i,x)) . z)
by A16, FUNCT_1:12
.=
(f1 - f2) /. ((reproj (i,x)) . z)
by A17, PARTFUN1:def 6
.=
(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 6
;
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:5; verum