let n be Nat; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for m being Nat of n st RAS is_semi_additive_in m holds

for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; :: thesis: for m being Nat of n st RAS is_semi_additive_in m holds

for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

let m be Nat of n; :: thesis: ( RAS is_semi_additive_in m implies for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q)) )

assume A1: RAS is_semi_additive_in m ; :: thesis: for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

let a, d be Point of RAS; :: thesis: for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

let p, q be Tuple of (n + 1),RAS; :: thesis: ( q = p +* (m,d) implies *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q)) )

set qq = q +* (m,(a @ d));

assume A2: q = p +* (m,d) ; :: thesis: *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

A3: q +* (m,(a @ d)) = p +* (m,(a @ d))

hence *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q)) by A1, A3; :: thesis: verum

for m being Nat of n st RAS is_semi_additive_in m holds

for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; :: thesis: for m being Nat of n st RAS is_semi_additive_in m holds

for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

let m be Nat of n; :: thesis: ( RAS is_semi_additive_in m implies for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q)) )

assume A1: RAS is_semi_additive_in m ; :: thesis: for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

let a, d be Point of RAS; :: thesis: for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

let p, q be Tuple of (n + 1),RAS; :: thesis: ( q = p +* (m,d) implies *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q)) )

set qq = q +* (m,(a @ d));

assume A2: q = p +* (m,d) ; :: thesis: *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

A3: q +* (m,(a @ d)) = p +* (m,(a @ d))

proof

q . m = d
by A2, Th10;
set pp = p +* (m,(a @ d));

for k being Nat of n holds (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k

end;for k being Nat of n holds (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k

proof

hence
q +* (m,(a @ d)) = p +* (m,(a @ d))
by Th9; :: thesis: verum
let k be Nat of n; :: thesis: (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k

end;now :: thesis: (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k

hence
(q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k
; :: thesis: verumend;

hence *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q)) by A1, A3; :: thesis: verum