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

(x +* (i,v)) . l = x . l by FUNCT_7:32; :: thesis: verum

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

thus
for l, i being Nat of n st l <> i holds
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;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

(x +* (i,v)) . l = x . l by FUNCT_7:32; :: thesis: verum