let r be Real; :: thesis: for G being non-trivial RealNormSpace-Sequence
for F being non trivial RealNormSpace
for f being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
r (#) (f * (reproj ((modetrans (G,i)),x))) = (r (#) f) * (reproj ((modetrans (G,i)),x))
let G be non-trivial RealNormSpace-Sequence; :: thesis: for F being non trivial RealNormSpace
for f being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
r (#) (f * (reproj ((modetrans (G,i)),x))) = (r (#) f) * (reproj ((modetrans (G,i)),x))
let F be non trivial RealNormSpace; :: thesis: for f being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
r (#) (f * (reproj ((modetrans (G,i)),x))) = (r (#) f) * (reproj ((modetrans (G,i)),x))
let f be PartFunc of (product G),F; :: thesis: for x being Point of (product G)
for i being set st i in dom G holds
r (#) (f * (reproj ((modetrans (G,i)),x))) = (r (#) f) * (reproj ((modetrans (G,i)),x))
let x be Point of (product G); :: thesis: for i being set st i in dom G holds
r (#) (f * (reproj ((modetrans (G,i)),x))) = (r (#) f) * (reproj ((modetrans (G,i)),x))
let i0 be set ; :: thesis: ( i0 in dom G implies r (#) (f * (reproj ((modetrans (G,i0)),x))) = (r (#) f) * (reproj ((modetrans (G,i0)),x)) )
assume i0 in dom G ; :: thesis: r (#) (f * (reproj ((modetrans (G,i0)),x))) = (r (#) f) * (reproj ((modetrans (G,i0)),x))
set i = modetrans (G,i0);
A1: dom (r (#) f) = dom f by VFUNCT_1:def 4;
A2: dom (r (#) (f * (reproj ((modetrans (G,i0)),x)))) = dom (f * (reproj ((modetrans (G,i0)),x))) by VFUNCT_1:def 4;
A3: dom (reproj ((modetrans (G,i0)),x)) = the carrier of (G . (modetrans (G,i0))) by FUNCT_2:def 1;
for s being Element of (G . (modetrans (G,i0))) holds
( s in dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) iff s in dom (f * (reproj ((modetrans (G,i0)),x))) )

proof

let s be Element of (G . (modetrans (G,i0))); :: thesis: ( s in dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) iff s in dom (f * (reproj ((modetrans (G,i0)),x))) )
( s in dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) iff (reproj ((modetrans (G,i0)),x)) . s in dom (r (#) f) ) by A3, FUNCT_1:11;
hence ( s in dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) iff s in dom (f * (reproj ((modetrans (G,i0)),x))) ) by A1, A3, FUNCT_1:11; :: thesis: verum

end;

then for s being set holds
( s in dom (r (#) (f * (reproj ((modetrans (G,i0)),x)))) iff s in dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) ) by A2;
then A4: dom (r (#) (f * (reproj ((modetrans (G,i0)),x)))) = dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) by TARSKI:1;
A5: for s being Element of (G . (modetrans (G,i0))) holds
( s in dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) iff (reproj ((modetrans (G,i0)),x)) . s in dom (r (#) f) )

proof

let s be Element of (G . (modetrans (G,i0))); :: thesis: ( s in dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) iff (reproj ((modetrans (G,i0)),x)) . s in dom (r (#) f) )
dom (reproj ((modetrans (G,i0)),x)) = the carrier of (G . (modetrans (G,i0))) by FUNCT_2:def 1;
hence ( s in dom ((r (#) f) * (reproj ((modetrans (G,i0)),x))) iff (reproj ((modetrans (G,i0)),x)) . s in dom (r (#) f) ) by FUNCT_1:11; :: thesis: verum

end;

for z being Element of (G . (modetrans (G,i0))) st z in dom (r (#) (f * (reproj ((modetrans (G,i0)),x)))) holds
(r (#) (f * (reproj ((modetrans (G,i0)),x)))) . z = ((r (#) f) * (reproj ((modetrans (G,i0)),x))) . z

proof

let z be Element of (G . (modetrans (G,i0))); :: thesis: ( z in dom (r (#) (f * (reproj ((modetrans (G,i0)),x)))) implies (r (#) (f * (reproj ((modetrans (G,i0)),x)))) . z = ((r (#) f) * (reproj ((modetrans (G,i0)),x))) . z )
assume A6: z in dom (r (#) (f * (reproj ((modetrans (G,i0)),x)))) ; :: thesis: (r (#) (f * (reproj ((modetrans (G,i0)),x)))) . z = ((r (#) f) * (reproj ((modetrans (G,i0)),x))) . z
then A7: z in dom (f * (reproj ((modetrans (G,i0)),x))) by VFUNCT_1:def 4;
A8: (reproj ((modetrans (G,i0)),x)) . z in dom f by A1, A5, A4, A6;
then A9: f /. ((reproj ((modetrans (G,i0)),x)) . z) = f . ((reproj ((modetrans (G,i0)),x)) . z) by PARTFUN1:def 6
.= (f * (reproj ((modetrans (G,i0)),x))) . z by A7, FUNCT_1:12
.= (f * (reproj ((modetrans (G,i0)),x))) /. z by A7, PARTFUN1:def 6 ;
A10: (r (#) (f * (reproj ((modetrans (G,i0)),x)))) . z = (r (#) (f * (reproj ((modetrans (G,i0)),x)))) /. z by A6, PARTFUN1:def 6
.= r * (f /. ((reproj ((modetrans (G,i0)),x)) . z)) by A6, A9, VFUNCT_1:def 4 ;
((r (#) f) * (reproj ((modetrans (G,i0)),x))) . z = (r (#) f) . ((reproj ((modetrans (G,i0)),x)) . z) by A4, A6, FUNCT_1:12
.= (r (#) f) /. ((reproj ((modetrans (G,i0)),x)) . z) by A1, A8, PARTFUN1:def 6
.= r * (f /. ((reproj ((modetrans (G,i0)),x)) . z)) by A1, A8, VFUNCT_1:def 4 ;
hence (r (#) (f * (reproj ((modetrans (G,i0)),x)))) . z = ((r (#) f) * (reproj ((modetrans (G,i0)),x))) . z by A10; :: thesis: verum

end;

hence r (#) (f * (reproj ((modetrans (G,i0)),x))) = (r (#) f) * (reproj ((modetrans (G,i0)),x)) by A4, PARTFUN1:5; :: thesis: verum