let n, i be Element of NAT ; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of
for v being Vector of
for x being Tuple of (n + 1),W holds
( ( for l being Nat of n st l = i holds
(x +* i,v) . l = v ) & ( for l, i being Nat of n st l <> i holds
(x +* i,v) . l = x . l ) )
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2; :: thesis: for W being ATLAS of
for v being Vector of
for x being Tuple of (n + 1),W holds
( ( for l being Nat of n st l = i holds
(x +* i,v) . l = v ) & ( for l, i being Nat of n st l <> i holds
(x +* i,v) . l = x . l ) )
let W be ATLAS of ; :: thesis: for v being Vector of
for x being Tuple of (n + 1),W holds
( ( for l being Nat of n st l = i holds
(x +* i,v) . l = v ) & ( for l, i being Nat of n st l <> i holds
(x +* i,v) . l = x . l ) )
let v be Vector of ; :: thesis: for x being Tuple of (n + 1),W holds
( ( for l being Nat of n st l = i holds
(x +* i,v) . l = v ) & ( for l, i being Nat of n st l <> i holds
(x +* i,v) . l = x . l ) )
let x be Tuple of (n + 1),W; :: thesis: ( ( for l being Nat of n st l = i holds
(x +* i,v) . l = v ) & ( for l, i being Nat of n st l <> i holds
(x +* i,v) . l = x . l ) )
thus for l being Nat of n st l = i holds
(x +* i,v) . l = v :: thesis: for l, i being Nat of n st l <> i holds
(x +* i,v) . l = x . l

proof

let l be Nat of n; :: thesis: ( l = i implies (x +* i,v) . l = v )
assume A1: l = i ; :: thesis: (x +* i,v) . l = v
l in Seg (n + 1) by Th8;
hence (x +* i,v) . l = v by A1, Lm1; :: thesis: verum

end;

thus for l, i being Nat of n st l <> i holds
(x +* i,v) . l = x . l by FUNCT_7:34; :: thesis: verum