let n be non zero Nat; :: thesis: for i being 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 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:36;

hence <>* (g * (reproj (i,y))) = f * (reproj (i,x)) by RELAT_1:36; :: thesis: verum

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 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:36;

hence <>* (g * (reproj (i,y))) = f * (reproj (i,x)) by RELAT_1:36; :: thesis: verum