let n, i be Nat; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for v being Vector of W
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 over n + 2; :: thesis: for W being ATLAS of RAS
for v being Vector of W
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 RAS; :: thesis: for v being Vector of W
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 W; :: 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 Th7;
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:32; :: thesis: verum