let m, n be non empty Element of NAT ; :: thesis: for j, i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z))
let j, i be Element of NAT ; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z))
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z))
let h be PartFunc of (REAL m),(REAL n); :: thesis: for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z))
let x be Point of (REAL-NS m); :: thesis: for z being Element of REAL m st f = h & x = z holds
((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z))
let z be Element of REAL m; :: thesis: ( f = h & x = z implies ((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z)) )
assume A1: ( f = h & x = z ) ; :: thesis: ((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z))
reconsider h1 = (proj 1,1) " as Function of REAL ,(REAL 1) by Th2;
<>* (((proj j,n) * h) * (reproj i,z)) = (h1 * ((proj j,n) * (h * (reproj i,z)))) * (proj 1,1) by RELAT_1:55
.= ((h1 * (proj j,n)) * (h * (reproj i,z))) * (proj 1,1) by RELAT_1:55
.= (h1 * (proj j,n)) * ((h * (reproj i,z)) * (proj 1,1)) by RELAT_1:55
.= (h1 * (proj j,n)) * (h * ((reproj i,z) * (proj 1,1))) by RELAT_1:55
.= (Proj j,n) * (h * ((reproj i,z) * (proj 1,1))) by Th11
.= (Proj j,n) * (h * (reproj i,x)) by A1, Th12 ;
hence ((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z)) by A1, RELAT_1:55; :: thesis: verum