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

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