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
proof
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;
hence p = q by FINSEQ_2:119; :: thesis: verum