let X, Y, W be RealNormSpace; for I being Function of X,Y
for f1, f2 being PartFunc of Y,W holds
( (f1 + f2) * I = (f1 * I) + (f2 * I) & (f1 - f2) * I = (f1 * I) - (f2 * I) )
let I be Function of X,Y; for f1, f2 being PartFunc of Y,W holds
( (f1 + f2) * I = (f1 * I) + (f2 * I) & (f1 - f2) * I = (f1 * I) - (f2 * I) )
let f1, f2 be PartFunc of Y,W; ( (f1 + f2) * I = (f1 * I) + (f2 * I) & (f1 - f2) * I = (f1 * I) - (f2 * I) )
set DI = the carrier of X;
A1:
dom I = the carrier of X
by FUNCT_2:def 1;
A2:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 1;
A3b:
for s being Element of the carrier of X holds
( s in dom ((f1 + f2) * I) iff s in dom ((f1 * I) + (f2 * I)) )
then A3:
for s being object holds
( s in dom ((f1 + f2) * I) iff s in dom ((f1 * I) + (f2 * I)) )
;
then A3a:
dom ((f1 + f2) * I) = dom ((f1 * I) + (f2 * I))
by TARSKI:2;
A4:
for z being Element of the carrier of X st z in dom ((f1 + f2) * I) holds
((f1 + f2) * I) . z = ((f1 * I) + (f2 * I)) . z
proof
let z be
Element of the
carrier of
X;
( z in dom ((f1 + f2) * I) implies ((f1 + f2) * I) . z = ((f1 * I) + (f2 * I)) . z )
assume A5:
z in dom ((f1 + f2) * I)
;
((f1 + f2) * I) . z = ((f1 * I) + (f2 * I)) . z
then A6:
I . z in dom (f1 + f2)
by FUNCT_1:11;
z in (dom (f1 * I)) /\ (dom (f2 * I))
by A3a, A5, VFUNCT_1:def 1;
then A7:
(
z in dom (f1 * I) &
z in dom (f2 * I) )
by XBOOLE_0:def 4;
A8:
I . z in (dom f1) /\ (dom f2)
by A2, A5, FUNCT_1:11;
then
I . z in dom f1
by XBOOLE_0:def 4;
then A9:
f1 /. (I . z) =
f1 . (I . z)
by PARTFUN1:def 6
.=
(f1 * I) . z
by A7, FUNCT_1:12
.=
(f1 * I) /. z
by A7, PARTFUN1:def 6
;
I . z in dom f2
by A8, XBOOLE_0:def 4;
then A10:
f2 /. (I . z) =
f2 . (I . z)
by PARTFUN1:def 6
.=
(f2 * I) . z
by A7, FUNCT_1:12
.=
(f2 * I) /. z
by A7, PARTFUN1:def 6
;
((f1 + f2) * I) . z =
(f1 + f2) . (I . z)
by A5, FUNCT_1:12
.=
(f1 + f2) /. (I . z)
by A6, PARTFUN1:def 6
.=
(f1 /. (I . z)) + (f2 /. (I . z))
by A6, VFUNCT_1:def 1
.=
((f1 * I) + (f2 * I)) /. z
by A3b, A5, A9, A10, VFUNCT_1:def 1
;
hence
((f1 + f2) * I) . z = ((f1 * I) + (f2 * I)) . z
by A3b, A5, PARTFUN1:def 6;
verum
end;
A11:
dom (f1 - f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 2;
A12b:
for s being Element of the carrier of X holds
( s in dom ((f1 - f2) * I) iff s in dom ((f1 * I) - (f2 * I)) )
then A12:
for s being object holds
( s in dom ((f1 - f2) * I) iff s in dom ((f1 * I) - (f2 * I)) )
;
then A12a:
dom ((f1 - f2) * I) = dom ((f1 * I) - (f2 * I))
by TARSKI:2;
for z being Element of the carrier of X st z in dom ((f1 - f2) * I) holds
((f1 - f2) * I) . z = ((f1 * I) - (f2 * I)) . z
proof
let z be
Element of the
carrier of
X;
( z in dom ((f1 - f2) * I) implies ((f1 - f2) * I) . z = ((f1 * I) - (f2 * I)) . z )
assume A13:
z in dom ((f1 - f2) * I)
;
((f1 - f2) * I) . z = ((f1 * I) - (f2 * I)) . z
then A14:
I . z in dom (f1 - f2)
by FUNCT_1:11;
z in (dom (f1 * I)) /\ (dom (f2 * I))
by A12a, A13, VFUNCT_1:def 2;
then A15:
(
z in dom (f1 * I) &
z in dom (f2 * I) )
by XBOOLE_0:def 4;
A16:
I . z in (dom f1) /\ (dom f2)
by A11, A13, FUNCT_1:11;
then
I . z in dom f1
by XBOOLE_0:def 4;
then A17:
f1 /. (I . z) =
f1 . (I . z)
by PARTFUN1:def 6
.=
(f1 * I) . z
by A15, FUNCT_1:12
.=
(f1 * I) /. z
by A15, PARTFUN1:def 6
;
I . z in dom f2
by A16, XBOOLE_0:def 4;
then A18:
f2 /. (I . z) =
f2 . (I . z)
by PARTFUN1:def 6
.=
(f2 * I) . z
by A15, FUNCT_1:12
.=
(f2 * I) /. z
by A15, PARTFUN1:def 6
;
thus ((f1 - f2) * I) . z =
(f1 - f2) . (I . z)
by A13, FUNCT_1:12
.=
(f1 - f2) /. (I . z)
by A14, PARTFUN1:def 6
.=
(f1 /. (I . z)) - (f2 /. (I . z))
by A14, VFUNCT_1:def 2
.=
((f1 * I) - (f2 * I)) /. z
by A12b, A13, A17, A18, VFUNCT_1:def 2
.=
((f1 * I) - (f2 * I)) . z
by A12b, A13, PARTFUN1:def 6
;
verum
end;
hence
( (f1 + f2) * I = (f1 * I) + (f2 * I) & (f1 - f2) * I = (f1 * I) - (f2 * I) )
by A3, A12, A4, TARSKI:2, PARTFUN1:5; verum