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