let n be Element of NAT ; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr of 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 of 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) )
assume A2: q = p +* m,d ; :: thesis: *' a,(p +* m,(a @ d)) = a @ (*' a,q)
then A3: q . m = d by Th12;
set qq = q +* m,(a @ d);
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

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 Th12;
hence (q +* m,(a @ d)) . k = (p +* m,(a @ d)) . k by A4, Th12; :: 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:34
.= p . k by A2, A5, FUNCT_7:34
.= (p +* m,(a @ d)) . k by A5, FUNCT_7:34 ;
:: 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 Th11; :: thesis: verum

end;

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