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))

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; :: thesis: (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k

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

per cases ( k = m or k <> m ) ;

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

(p +* (m,(a @ d))) . m = a @ d by Th10;
hence (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k by A4, Th10; :: thesis: verum

end;

suppose A5: k <> m ; :: thesis: (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k

hence (q +* (m,(a @ d))) . k = q . k by FUNCT_7:32
.= p . k by A2, A5, FUNCT_7:32
.= (p +* (m,(a @ d))) . k by A5, FUNCT_7:32 ;
:: thesis: verum

end;

end;

end;

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

end;

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

end;

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