reconsider x0 = x as Element of product (carr X) ;
A1: reproj (i,x0) is Function of ((carr X) . i),(product (carr X)) ;
(carr X) . i = the carrier of (X . i) by PRVECT_1:def 11;
hence ex b₁ being Function of (X . i),(product X) ex x0 being Element of product (carr X) st
( x0 = x & b₁ = reproj (i,x0) ) by A1; :: thesis: verum