let n be Nat; 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; 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; ( 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
; 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; 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; ( 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)
; *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))
A3:
q +* (m,(a @ d)) = p +* (m,(a @ d))
proof
set pp =
p +* (
m,
(a @ d));
for
k being
Nat of
n holds
(q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k
proof
let k be
Nat of
n;
(q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k
hence
(q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k
;
verum
end;
hence
q +* (
m,
(a @ d))
= p +* (
m,
(a @ d))
by Th9;
verum
end;
q . m = d
by A2, Th10;
hence
*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))
by A1, A3; verum