let m be non zero Nat; :: thesis: for x, y being Element of REAL m
for i being 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 Nat
for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds
(proj (i,m)) . y = xi
let i be 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 )
reconsider xx = xi as Element of REAL by XREAL_0:def 1;
assume A1: ( 1 <= i & i <= m & y = (reproj (i,x)) . xi ) ; :: thesis: (proj (i,m)) . y = xi
then A2: y = Replace (x,i,xx) by PDIFF_1:def 5;
A3: ( len x = m & len y = m ) by CARD_1:def 7;
then A4: i in dom y by A1, FINSEQ_3:25;
y /. i = xi by A1, A2, A3, FINSEQ_7:8;
then y . i = xi by A4, PARTFUN1:def 6;
hence (proj (i,m)) . y = xi by PDIFF_1:def 1; :: thesis: verum