let G be RealNormSpace-Sequence; for F being RealNormSpace
for f1, f2 being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
( (f1 + f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) + (f2 * (reproj ((In (i,(dom G))),x))) & (f1 - f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) - (f2 * (reproj ((In (i,(dom G))),x))) )
let F be RealNormSpace; for f1, f2 being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
( (f1 + f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) + (f2 * (reproj ((In (i,(dom G))),x))) & (f1 - f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) - (f2 * (reproj ((In (i,(dom G))),x))) )
let f1, f2 be PartFunc of (product G),F; for x being Point of (product G)
for i being set st i in dom G holds
( (f1 + f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) + (f2 * (reproj ((In (i,(dom G))),x))) & (f1 - f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) - (f2 * (reproj ((In (i,(dom G))),x))) )
let x be Point of (product G); for i being set st i in dom G holds
( (f1 + f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) + (f2 * (reproj ((In (i,(dom G))),x))) & (f1 - f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) - (f2 * (reproj ((In (i,(dom G))),x))) )
let i0 be set ; ( i0 in dom G implies ( (f1 + f2) * (reproj ((In (i0,(dom G))),x)) = (f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x))) & (f1 - f2) * (reproj ((In (i0,(dom G))),x)) = (f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x))) ) )
assume
i0 in dom G
; ( (f1 + f2) * (reproj ((In (i0,(dom G))),x)) = (f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x))) & (f1 - f2) * (reproj ((In (i0,(dom G))),x)) = (f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x))) )
set i = In (i0,(dom G));
A1:
dom (reproj ((In (i0,(dom G))),x)) = the carrier of (G . (In (i0,(dom G))))
by FUNCT_2:def 1;
A2:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 1;
A3b:
for s being Element of (G . (In (i0,(dom G)))) holds
( s in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) iff s in dom ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) )
proof
let s be
Element of
(G . (In (i0,(dom G))));
( s in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) iff s in dom ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) )
(
s in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) iff
(reproj ((In (i0,(dom G))),x)) . s in (dom f1) /\ (dom f2) )
by A2, A1, FUNCT_1:11;
then
(
s in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) iff (
(reproj ((In (i0,(dom G))),x)) . s in dom f1 &
(reproj ((In (i0,(dom G))),x)) . s in dom f2 ) )
by XBOOLE_0:def 4;
then
(
s in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) iff (
s in dom (f1 * (reproj ((In (i0,(dom G))),x))) &
s in dom (f2 * (reproj ((In (i0,(dom G))),x))) ) )
by A1, FUNCT_1:11;
then
(
s in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) iff
s in (dom (f1 * (reproj ((In (i0,(dom G))),x)))) /\ (dom (f2 * (reproj ((In (i0,(dom G))),x)))) )
by XBOOLE_0:def 4;
hence
(
s in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) iff
s in dom ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) )
by VFUNCT_1:def 1;
verum
end;
then A3:
for s being object holds
( s in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) iff s in dom ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) )
;
then A3a:
dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) = dom ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x))))
by TARSKI:2;
A4:
for z being Element of (G . (In (i0,(dom G)))) st z in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) holds
((f1 + f2) * (reproj ((In (i0,(dom G))),x))) . z = ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) . z
proof
let z be
Element of
(G . (In (i0,(dom G))));
( z in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) implies ((f1 + f2) * (reproj ((In (i0,(dom G))),x))) . z = ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) . z )
assume A5:
z in dom ((f1 + f2) * (reproj ((In (i0,(dom G))),x)))
;
((f1 + f2) * (reproj ((In (i0,(dom G))),x))) . z = ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) . z
then A6:
(reproj ((In (i0,(dom G))),x)) . z in dom (f1 + f2)
by FUNCT_1:11;
z in (dom (f1 * (reproj ((In (i0,(dom G))),x)))) /\ (dom (f2 * (reproj ((In (i0,(dom G))),x))))
by A3a, A5, VFUNCT_1:def 1;
then A7:
(
z in dom (f1 * (reproj ((In (i0,(dom G))),x))) &
z in dom (f2 * (reproj ((In (i0,(dom G))),x))) )
by XBOOLE_0:def 4;
A8:
(reproj ((In (i0,(dom G))),x)) . z in (dom f1) /\ (dom f2)
by A2, A5, FUNCT_1:11;
then
(reproj ((In (i0,(dom G))),x)) . z in dom f1
by XBOOLE_0:def 4;
then A9:
f1 /. ((reproj ((In (i0,(dom G))),x)) . z) =
f1 . ((reproj ((In (i0,(dom G))),x)) . z)
by PARTFUN1:def 6
.=
(f1 * (reproj ((In (i0,(dom G))),x))) . z
by A7, FUNCT_1:12
.=
(f1 * (reproj ((In (i0,(dom G))),x))) /. z
by A7, PARTFUN1:def 6
;
(reproj ((In (i0,(dom G))),x)) . z in dom f2
by A8, XBOOLE_0:def 4;
then A10:
f2 /. ((reproj ((In (i0,(dom G))),x)) . z) =
f2 . ((reproj ((In (i0,(dom G))),x)) . z)
by PARTFUN1:def 6
.=
(f2 * (reproj ((In (i0,(dom G))),x))) . z
by A7, FUNCT_1:12
.=
(f2 * (reproj ((In (i0,(dom G))),x))) /. z
by A7, PARTFUN1:def 6
;
((f1 + f2) * (reproj ((In (i0,(dom G))),x))) . z =
(f1 + f2) . ((reproj ((In (i0,(dom G))),x)) . z)
by A5, FUNCT_1:12
.=
(f1 + f2) /. ((reproj ((In (i0,(dom G))),x)) . z)
by A6, PARTFUN1:def 6
.=
(f1 /. ((reproj ((In (i0,(dom G))),x)) . z)) + (f2 /. ((reproj ((In (i0,(dom G))),x)) . z))
by A6, VFUNCT_1:def 1
.=
((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) /. z
by A3b, A5, A9, A10, VFUNCT_1:def 1
;
hence
((f1 + f2) * (reproj ((In (i0,(dom G))),x))) . z = ((f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))) . 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 (G . (In (i0,(dom G)))) holds
( s in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) iff s in dom ((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) )
proof
let s be
Element of
(G . (In (i0,(dom G))));
( s in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) iff s in dom ((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) )
(
s in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) iff
(reproj ((In (i0,(dom G))),x)) . s in (dom f1) /\ (dom f2) )
by A11, A1, FUNCT_1:11;
then
(
s in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) iff (
(reproj ((In (i0,(dom G))),x)) . s in dom f1 &
(reproj ((In (i0,(dom G))),x)) . s in dom f2 ) )
by XBOOLE_0:def 4;
then
(
s in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) iff (
s in dom (f1 * (reproj ((In (i0,(dom G))),x))) &
s in dom (f2 * (reproj ((In (i0,(dom G))),x))) ) )
by A1, FUNCT_1:11;
then
(
s in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) iff
s in (dom (f1 * (reproj ((In (i0,(dom G))),x)))) /\ (dom (f2 * (reproj ((In (i0,(dom G))),x)))) )
by XBOOLE_0:def 4;
hence
(
s in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) iff
s in dom ((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) )
by VFUNCT_1:def 2;
verum
end;
then A12:
for s being object holds
( s in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) iff s in dom ((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) )
;
then A12a:
dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) = dom ((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x))))
by TARSKI:2;
for z being Element of (G . (In (i0,(dom G)))) st z in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) holds
((f1 - f2) * (reproj ((In (i0,(dom G))),x))) . z = ((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) . z
proof
let z be
Element of
(G . (In (i0,(dom G))));
( z in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) implies ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) . z = ((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) . z )
assume A13:
z in dom ((f1 - f2) * (reproj ((In (i0,(dom G))),x)))
;
((f1 - f2) * (reproj ((In (i0,(dom G))),x))) . z = ((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) . z
then A14:
(reproj ((In (i0,(dom G))),x)) . z in dom (f1 - f2)
by FUNCT_1:11;
z in (dom (f1 * (reproj ((In (i0,(dom G))),x)))) /\ (dom (f2 * (reproj ((In (i0,(dom G))),x))))
by A12a, A13, VFUNCT_1:def 2;
then A15:
(
z in dom (f1 * (reproj ((In (i0,(dom G))),x))) &
z in dom (f2 * (reproj ((In (i0,(dom G))),x))) )
by XBOOLE_0:def 4;
A16:
(reproj ((In (i0,(dom G))),x)) . z in (dom f1) /\ (dom f2)
by A11, A13, FUNCT_1:11;
then
(reproj ((In (i0,(dom G))),x)) . z in dom f1
by XBOOLE_0:def 4;
then A17:
f1 /. ((reproj ((In (i0,(dom G))),x)) . z) =
f1 . ((reproj ((In (i0,(dom G))),x)) . z)
by PARTFUN1:def 6
.=
(f1 * (reproj ((In (i0,(dom G))),x))) . z
by A15, FUNCT_1:12
.=
(f1 * (reproj ((In (i0,(dom G))),x))) /. z
by A15, PARTFUN1:def 6
;
(reproj ((In (i0,(dom G))),x)) . z in dom f2
by A16, XBOOLE_0:def 4;
then A18:
f2 /. ((reproj ((In (i0,(dom G))),x)) . z) =
f2 . ((reproj ((In (i0,(dom G))),x)) . z)
by PARTFUN1:def 6
.=
(f2 * (reproj ((In (i0,(dom G))),x))) . z
by A15, FUNCT_1:12
.=
(f2 * (reproj ((In (i0,(dom G))),x))) /. z
by A15, PARTFUN1:def 6
;
thus ((f1 - f2) * (reproj ((In (i0,(dom G))),x))) . z =
(f1 - f2) . ((reproj ((In (i0,(dom G))),x)) . z)
by A13, FUNCT_1:12
.=
(f1 - f2) /. ((reproj ((In (i0,(dom G))),x)) . z)
by A14, PARTFUN1:def 6
.=
(f1 /. ((reproj ((In (i0,(dom G))),x)) . z)) - (f2 /. ((reproj ((In (i0,(dom G))),x)) . z))
by A14, VFUNCT_1:def 2
.=
((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) /. z
by A12b, A13, A17, A18, VFUNCT_1:def 2
.=
((f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))) . z
by A12b, A13, PARTFUN1:def 6
;
verum
end;
hence
( (f1 + f2) * (reproj ((In (i0,(dom G))),x)) = (f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x))) & (f1 - f2) * (reproj ((In (i0,(dom G))),x)) = (f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x))) )
by A3, A12, A4, TARSKI:2, PARTFUN1:5; verum