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

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

p = q

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; :: thesis: for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds p . m = q . m ) holds

p = q

let p, q be Tuple of (n + 1),RAS; :: thesis: ( ( for m being Nat of n holds p . m = q . m ) implies p = q )

assume A1: for m being Nat of n holds p . m = q . m ; :: thesis: p = q

for j being Nat st j in Seg (n + 1) holds

p . j = q . j

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

p = q

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; :: thesis: for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds p . m = q . m ) holds

p = q

let p, q be Tuple of (n + 1),RAS; :: thesis: ( ( for m being Nat of n holds p . m = q . m ) implies p = q )

assume A1: for m being Nat of n holds p . m = q . m ; :: thesis: p = q

for j being Nat st j in Seg (n + 1) holds

p . j = q . j

proof

hence
p = q
by FINSEQ_2:119; :: thesis: verum
let j be Nat; :: thesis: ( j in Seg (n + 1) implies p . j = q . j )

assume j in Seg (n + 1) ; :: thesis: p . j = q . j

then reconsider j = j as Nat of n by Th7;

p . j = q . j by A1;

hence p . j = q . j ; :: thesis: verum

end;assume j in Seg (n + 1) ; :: thesis: p . j = q . j

then reconsider j = j as Nat of n by Th7;

p . j = q . j by A1;

hence p . j = q . j ; :: thesis: verum