let n be non empty Element of NAT ; :: thesis: for i being Element of NAT
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj i,y)) = f * (reproj i,x)
let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj i,y)) = f * (reproj i,x)
let f be PartFunc of (REAL-NS n),(REAL-NS 1); :: thesis: for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj i,y)) = f * (reproj i,x)
let g be PartFunc of (REAL n),REAL ; :: thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj i,y)) = f * (reproj i,x)
let x be Point of (REAL-NS n); :: thesis: for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj i,y)) = f * (reproj i,x)
let y be Element of REAL n; :: thesis: ( f = <>* g & x = y implies <>* (g * (reproj i,y)) = f * (reproj i,x) )
reconsider h = (proj 1,1) " as Function of REAL ,(REAL 1) by Th2;
assume that
A1: f = <>* g and
A2: x = y ; :: thesis: <>* (g * (reproj i,y)) = f * (reproj i,x)
(reproj i,y) * (proj 1,1) = reproj i,x by A2, Th12;
then ((h * g) * (reproj i,y)) * (proj 1,1) = f * (reproj i,x) by A1, RELAT_1:55;
hence <>* (g * (reproj i,y)) = f * (reproj i,x) by RELAT_1:55; :: thesis: verum