let m, n be non zero Nat; :: thesis: for i being Nat
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
let i be Nat; :: thesis: for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
let r be Real; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
let x be Point of (REAL-NS m); :: thesis: r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
A1: dom (r (#) f) = dom f by VFUNCT_1:def 4;
A2: dom (r (#) (f * (reproj (i,x)))) = dom (f * (reproj (i,x))) by VFUNCT_1:def 4;
A3: dom (reproj (i,x)) = the carrier of (REAL-NS 1) by FUNCT_2:def 1;
for s being Element of (REAL-NS 1) holds
( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) )

proof

let s be Element of (REAL-NS 1); :: thesis: ( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) )
( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) ) by A3, FUNCT_1:11;
hence ( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) ) by A1, A3, FUNCT_1:11; :: thesis: verum

end;

then for s being object holds
( s in dom (r (#) (f * (reproj (i,x)))) iff s in dom ((r (#) f) * (reproj (i,x))) ) by A2;
then A4: dom (r (#) (f * (reproj (i,x)))) = dom ((r (#) f) * (reproj (i,x))) by TARSKI:2;
A5: for s being Element of (REAL-NS 1) holds
( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) )

proof

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

end;

for z being Element of (REAL-NS 1) st z in dom (r (#) (f * (reproj (i,x)))) holds
(r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z

proof

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

end;

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