let m be non empty Element of NAT ; :: thesis: for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi holds
(proj i,m) . y = xi
let x, y be Element of REAL m; :: thesis: for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi holds
(proj i,m) . y = xi
let i be Element of NAT ; :: thesis: for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi holds
(proj i,m) . y = xi
let xi be Real; :: thesis: ( 1 <= i & i <= m & y = (reproj i,x) . xi implies (proj i,m) . y = xi )
assume A1: ( 1 <= i & i <= m & y = (reproj i,x) . xi ) ; :: thesis: (proj i,m) . y = xi
then A2: y = Replace x,i,xi by PDIFF_1:def 5;
A3: ( len x = m & len y = m ) by FINSEQ_1:def 18;
then A4: i in dom y by A1, FINSEQ_3:27;
y /. i = xi by A1, A2, A3, FINSEQ_7:10;
then y . i = xi by A4, PARTFUN1:def 8;
hence (proj i,m) . y = xi by PDIFF_1:def 1; :: thesis: verum