let n, m be non empty Element of NAT ; :: thesis: for i being Element of 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 Element of 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 (reproj i,x) = the carrier of (REAL-NS 1) by FUNCT_2:def 1;
A3: 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:21; :: thesis: verum

end;

A4: 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 A2, FUNCT_1:21;
hence ( s in dom ((r (#) f) * (reproj i,x)) iff s in dom (f * (reproj i,x)) ) by A1, A2, FUNCT_1:21; :: thesis: verum

end;

A5: dom (r (#) (f * (reproj i,x))) = dom ((r (#) f) * (reproj i,x))

proof

dom (r (#) (f * (reproj i,x))) = dom (f * (reproj i,x)) by VFUNCT_1:def 4;
then for s being set holds
( s in dom (r (#) (f * (reproj i,x))) iff s in dom ((r (#) f) * (reproj i,x)) ) by A4;
hence dom (r (#) (f * (reproj i,x))) = dom ((r (#) f) * (reproj i,x)) by TARSKI:2; :: 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: (reproj i,x) . z in dom f by A1, A3, A5;
A8: z in dom (f * (reproj i,x)) by A6, VFUNCT_1:def 4;
A9: f /. ((reproj i,x) . z) = f . ((reproj i,x) . z) by A7, PARTFUN1:def 8
.= (f * (reproj i,x)) . z by A8, FUNCT_1:22
.= (f * (reproj i,x)) /. z by A8, PARTFUN1:def 8 ;
A10: (r (#) (f * (reproj i,x))) . z = (r (#) (f * (reproj i,x))) /. z by A6, PARTFUN1:def 8
.= 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 A5, A6, FUNCT_1:22
.= (r (#) f) /. ((reproj i,x) . z) by A1, A7, PARTFUN1:def 8
.= r * (f /. ((reproj i,x) . z)) by A1, A7, 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 A5, PARTFUN1:34; :: thesis: verum