let m, n be non empty Element of NAT ; :: thesis: for j, i being Element of NAT
for f being PartFunc of ,
for h being PartFunc of ,
for x being Point of
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 ,
for h being PartFunc of ,
for x being Point of
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 ,; :: thesis: for h being PartFunc of ,
for x being Point of
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 ,; :: thesis: for x being Point of
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 ; :: 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: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 A2, Th12 ;
hence ((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z)) by A1, RELAT_1:55; :: thesis: verum