let n, i be Nat; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for d being Point of RAS
for p being Tuple of (n + 1),RAS
for l being Nat of n st l = i holds
(p +* (i,d)) . l = d
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; :: thesis: for d being Point of RAS
for p being Tuple of (n + 1),RAS
for l being Nat of n st l = i holds
(p +* (i,d)) . l = d
let d be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS
for l being Nat of n st l = i holds
(p +* (i,d)) . l = d
let p be Tuple of (n + 1),RAS; :: thesis: for l being Nat of n st l = i holds
(p +* (i,d)) . l = d
let l be Nat of n; :: thesis: ( l = i implies (p +* (i,d)) . l = d )
assume A1: l = i ; :: thesis: (p +* (i,d)) . l = d
l in Seg (n + 1) by Th7;
hence (p +* (i,d)) . l = d by A1, Lm1; :: thesis: verum