let M be non empty set ; for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X being set
for f1 being PartFunc of M,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let V be ComplexNormSpace; for f2 being PartFunc of M,V
for X being set
for f1 being PartFunc of M,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let f2 be PartFunc of M,V; for X being set
for f1 being PartFunc of M,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let X be set ; for f1 being PartFunc of M,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let f1 be PartFunc of M,COMPLEX; ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
A1:
now for c being Element of M st c in dom ((f1 (#) f2) | X) holds
((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. clet c be
Element of
M;
( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. c )assume A2:
c in dom ((f1 (#) f2) | X)
;
((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. cthen A3:
c in (dom (f1 (#) f2)) /\ X
by RELAT_1:61;
then A4:
c in X
by XBOOLE_0:def 4;
A5:
c in dom (f1 (#) f2)
by A3, XBOOLE_0:def 4;
then A6:
c in (dom f1) /\ (dom f2)
by Def1;
then A7:
c in dom f1
by XBOOLE_0:def 4;
then
c in (dom f1) /\ X
by A4, XBOOLE_0:def 4;
then A8:
c in dom (f1 | X)
by RELAT_1:61;
then A9:
(f1 | X) /. c =
(f1 | X) . c
by PARTFUN1:def 6
.=
f1 . c
by A8, FUNCT_1:47
.=
f1 /. c
by A7, PARTFUN1:def 6
;
c in dom f2
by A6, XBOOLE_0:def 4;
then
c in (dom f2) /\ X
by A4, XBOOLE_0:def 4;
then A10:
c in dom (f2 | X)
by RELAT_1:61;
then
c in (dom (f1 | X)) /\ (dom (f2 | X))
by A8, XBOOLE_0:def 4;
then A11:
c in dom ((f1 | X) (#) (f2 | X))
by Def1;
thus ((f1 (#) f2) | X) /. c =
(f1 (#) f2) /. c
by A2, PARTFUN2:15
.=
(f1 /. c) * (f2 /. c)
by A5, Def1
.=
((f1 | X) /. c) * ((f2 | X) /. c)
by A10, A9, PARTFUN2:15
.=
((f1 | X) (#) (f2 | X)) /. c
by A11, Def1
;
verum end;
dom ((f1 (#) f2) | X) =
(dom (f1 (#) f2)) /\ X
by RELAT_1:61
.=
((dom f1) /\ (dom f2)) /\ (X /\ X)
by Def1
.=
(dom f1) /\ ((dom f2) /\ (X /\ X))
by XBOOLE_1:16
.=
(dom f1) /\ (((dom f2) /\ X) /\ X)
by XBOOLE_1:16
.=
(dom f1) /\ (X /\ (dom (f2 | X)))
by RELAT_1:61
.=
((dom f1) /\ X) /\ (dom (f2 | X))
by XBOOLE_1:16
.=
(dom (f1 | X)) /\ (dom (f2 | X))
by RELAT_1:61
.=
dom ((f1 | X) (#) (f2 | X))
by Def1
;
hence
(f1 (#) f2) | X = (f1 | X) (#) (f2 | X)
by A1, PARTFUN2:1; ( (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
A12:
now for c being Element of M st c in dom ((f1 (#) f2) | X) holds
((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. clet c be
Element of
M;
( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c )assume A13:
c in dom ((f1 (#) f2) | X)
;
((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. cthen A14:
c in (dom (f1 (#) f2)) /\ X
by RELAT_1:61;
then A15:
c in dom (f1 (#) f2)
by XBOOLE_0:def 4;
then A16:
c in (dom f1) /\ (dom f2)
by Def1;
then A17:
c in dom f1
by XBOOLE_0:def 4;
c in X
by A14, XBOOLE_0:def 4;
then
c in (dom f1) /\ X
by A17, XBOOLE_0:def 4;
then A18:
c in dom (f1 | X)
by RELAT_1:61;
then A19:
(f1 | X) /. c =
(f1 | X) . c
by PARTFUN1:def 6
.=
f1 . c
by A18, FUNCT_1:47
;
c in dom f2
by A16, XBOOLE_0:def 4;
then
c in (dom (f1 | X)) /\ (dom f2)
by A18, XBOOLE_0:def 4;
then A20:
c in dom ((f1 | X) (#) f2)
by Def1;
thus ((f1 (#) f2) | X) /. c =
(f1 (#) f2) /. c
by A13, PARTFUN2:15
.=
(f1 /. c) * (f2 /. c)
by A15, Def1
.=
((f1 | X) /. c) * (f2 /. c)
by A17, A19, PARTFUN1:def 6
.=
((f1 | X) (#) f2) /. c
by A20, Def1
;
verum end;
dom ((f1 (#) f2) | X) =
(dom (f1 (#) f2)) /\ X
by RELAT_1:61
.=
((dom f1) /\ (dom f2)) /\ X
by Def1
.=
((dom f1) /\ X) /\ (dom f2)
by XBOOLE_1:16
.=
(dom (f1 | X)) /\ (dom f2)
by RELAT_1:61
.=
dom ((f1 | X) (#) f2)
by Def1
;
hence
(f1 (#) f2) | X = (f1 | X) (#) f2
by A12, PARTFUN2:1; (f1 (#) f2) | X = f1 (#) (f2 | X)
dom ((f1 (#) f2) | X) =
(dom (f1 (#) f2)) /\ X
by RELAT_1:61
.=
((dom f1) /\ (dom f2)) /\ X
by Def1
.=
(dom f1) /\ ((dom f2) /\ X)
by XBOOLE_1:16
.=
(dom f1) /\ (dom (f2 | X))
by RELAT_1:61
.=
dom (f1 (#) (f2 | X))
by Def1
;
hence
(f1 (#) f2) | X = f1 (#) (f2 | X)
by A21, PARTFUN2:1; verum