let r be Real; :: thesis: for G being RealNormSpace-Sequence
for F being 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 ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),x))
let G be RealNormSpace-Sequence; :: thesis: for F being 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 ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),x))
let F be 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 ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),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 ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),x))
let x be Point of (product G); :: thesis: for i being set st i in dom G holds
r (#) (f * (reproj ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),x))
let i0 be set ; :: thesis: ( i0 in dom G implies r (#) (f * (reproj ((In (i0,(dom G))),x))) = (r (#) f) * (reproj ((In (i0,(dom G))),x)) )
assume i0 in dom G ; :: thesis: r (#) (f * (reproj ((In (i0,(dom G))),x))) = (r (#) f) * (reproj ((In (i0,(dom G))),x))
set i = In (i0,(dom G));
A1: dom (r (#) f) = dom f by VFUNCT_1:def 4;
A2: dom (r (#) (f * (reproj ((In (i0,(dom G))),x)))) = dom (f * (reproj ((In (i0,(dom G))),x))) by VFUNCT_1:def 4;
A3: dom (reproj ((In (i0,(dom G))),x)) = the carrier of (G . (In (i0,(dom G)))) by FUNCT_2:def 1;
A4b: for s being Element of (G . (In (i0,(dom G)))) holds
( s in dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) iff s in dom (f * (reproj ((In (i0,(dom G))),x))) )
proof
let s be Element of (G . (In (i0,(dom G)))); :: thesis: ( s in dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) iff s in dom (f * (reproj ((In (i0,(dom G))),x))) )
( s in dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) iff (reproj ((In (i0,(dom G))),x)) . s in dom (r (#) f) ) by A3, FUNCT_1:11;
hence ( s in dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) iff s in dom (f * (reproj ((In (i0,(dom G))),x))) ) by A1, A3, FUNCT_1:11; :: thesis: verum
end;
then A4: for s being object holds
( s in dom (r (#) (f * (reproj ((In (i0,(dom G))),x)))) iff s in dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) ) by A2;
then A4a: dom (r (#) (f * (reproj ((In (i0,(dom G))),x)))) = dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) by TARSKI:2;
A5: for s being Element of (G . (In (i0,(dom G)))) holds
( s in dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) iff (reproj ((In (i0,(dom G))),x)) . s in dom (r (#) f) )
proof
let s be Element of (G . (In (i0,(dom G)))); :: thesis: ( s in dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) iff (reproj ((In (i0,(dom G))),x)) . s in dom (r (#) f) )
dom (reproj ((In (i0,(dom G))),x)) = the carrier of (G . (In (i0,(dom G)))) by FUNCT_2:def 1;
hence ( s in dom ((r (#) f) * (reproj ((In (i0,(dom G))),x))) iff (reproj ((In (i0,(dom G))),x)) . s in dom (r (#) f) ) by FUNCT_1:11; :: thesis: verum
end;
for z being Element of (G . (In (i0,(dom G)))) st z in dom (r (#) (f * (reproj ((In (i0,(dom G))),x)))) holds
(r (#) (f * (reproj ((In (i0,(dom G))),x)))) . z = ((r (#) f) * (reproj ((In (i0,(dom G))),x))) . z
proof
let z be Element of (G . (In (i0,(dom G)))); :: thesis: ( z in dom (r (#) (f * (reproj ((In (i0,(dom G))),x)))) implies (r (#) (f * (reproj ((In (i0,(dom G))),x)))) . z = ((r (#) f) * (reproj ((In (i0,(dom G))),x))) . z )
assume A6: z in dom (r (#) (f * (reproj ((In (i0,(dom G))),x)))) ; :: thesis: (r (#) (f * (reproj ((In (i0,(dom G))),x)))) . z = ((r (#) f) * (reproj ((In (i0,(dom G))),x))) . z
then A7: z in dom (f * (reproj ((In (i0,(dom G))),x))) by VFUNCT_1:def 4;
A9: f /. ((reproj ((In (i0,(dom G))),x)) . z) = f . ((reproj ((In (i0,(dom G))),x)) . z) by A1, A5, A4a, A6, PARTFUN1:def 6
.= (f * (reproj ((In (i0,(dom G))),x))) . z by A7, FUNCT_1:12
.= (f * (reproj ((In (i0,(dom G))),x))) /. z by A7, PARTFUN1:def 6 ;
A10: (r (#) (f * (reproj ((In (i0,(dom G))),x)))) . z = (r (#) (f * (reproj ((In (i0,(dom G))),x)))) /. z by A6, PARTFUN1:def 6
.= r * (f /. ((reproj ((In (i0,(dom G))),x)) . z)) by A6, A9, VFUNCT_1:def 4 ;
((r (#) f) * (reproj ((In (i0,(dom G))),x))) . z = (r (#) f) . ((reproj ((In (i0,(dom G))),x)) . z) by A2, A4b, A6, FUNCT_1:12
.= (r (#) f) /. ((reproj ((In (i0,(dom G))),x)) . z) by A5, A4a, A6, PARTFUN1:def 6
.= r * (f /. ((reproj ((In (i0,(dom G))),x)) . z)) by A5, A4a, A6, VFUNCT_1:def 4 ;
hence (r (#) (f * (reproj ((In (i0,(dom G))),x)))) . z = ((r (#) f) * (reproj ((In (i0,(dom G))),x))) . z by A10; :: thesis: verum
end;
hence r (#) (f * (reproj ((In (i0,(dom G))),x))) = (r (#) f) * (reproj ((In (i0,(dom G))),x)) by A4, TARSKI:2, PARTFUN1:5; :: thesis: verum