let X be non-empty non empty FinSequence; :: thesis: for x being Element of product X
for i being Element of dom X
for r being object st r in X . i holds
((reproj (i,x)) . r) . i = r
let x be Element of product X; :: thesis: for i being Element of dom X
for r being object st r in X . i holds
((reproj (i,x)) . r) . i = r
let i be Element of dom X; :: thesis: for r being object st r in X . i holds
((reproj (i,x)) . r) . i = r
let r be object ; :: thesis: ( r in X . i implies ((reproj (i,x)) . r) . i = r )
assume r in X . i ; :: thesis: ((reproj (i,x)) . r) . i = r
then A1: (reproj (i,x)) . r = x +* (i,r) by Def1;
ex g being Function st
( x = g & dom g = dom X & ( for j being object st j in dom X holds
g . j in X . j ) ) by CARD_3:def 5;
hence ((reproj (i,x)) . r) . i = r by A1, FUNCT_7:31; :: thesis: verum