let m, n be non zero Nat; :: thesis: for i, j being 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 i, j be 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))) )
reconsider h1 = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;
assume that
A1: f = h and
A2: x = z ; :: thesis: ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
<>* (((proj (j,n)) * h) * (reproj (i,z))) = (h1 * ((proj (j,n)) * (h * (reproj (i,z))))) * (proj (1,1)) by RELAT_1:36
.= ((h1 * (proj (j,n))) * (h * (reproj (i,z)))) * (proj (1,1)) by RELAT_1:36
.= (h1 * (proj (j,n))) * ((h * (reproj (i,z))) * (proj (1,1))) by RELAT_1:36
.= (h1 * (proj (j,n))) * (h * ((reproj (i,z)) * (proj (1,1)))) by RELAT_1:36
.= (Proj (j,n)) * (h * ((reproj (i,z)) * (proj (1,1)))) by Th11
.= (Proj (j,n)) * (h * (reproj (i,x))) by A2, Th12 ;
hence ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) by A1, RELAT_1:36; :: thesis: verum