let X be non-empty non empty FinSequence; :: thesis: for x being Element of product X
for i being Element of dom X holds (reproj (i,x)) . (x . i) = x
let x be Element of product X; :: thesis: for i being Element of dom X holds (reproj (i,x)) . (x . i) = x
let i be Element of dom X; :: thesis: (reproj (i,x)) . (x . i) = x
(reproj (i,x)) . (x . i) = x +* (i,(x . i)) by Def1;
hence (reproj (i,x)) . (x . i) = x by FUNCT_7:35; :: thesis: verum