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

for W being ATLAS of RAS

for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds

x = y

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

for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds

x = y

let W be ATLAS of RAS; :: thesis: for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds

x = y

let x, y be Tuple of (n + 1),W; :: thesis: ( ( for m being Nat of n holds x . m = y . m ) implies x = y )

assume A1: for m being Nat of n holds x . m = y . m ; :: thesis: x = y

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

x . j = y . j

for W being ATLAS of RAS

for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds

x = y

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

for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds

x = y

let W be ATLAS of RAS; :: thesis: for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds

x = y

let x, y be Tuple of (n + 1),W; :: thesis: ( ( for m being Nat of n holds x . m = y . m ) implies x = y )

assume A1: for m being Nat of n holds x . m = y . m ; :: thesis: x = y

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

x . j = y . j

proof

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

assume j in Seg (n + 1) ; :: thesis: x . j = y . j

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

x . j = y . j by A1;

hence x . j = y . j ; :: thesis: verum

end;assume j in Seg (n + 1) ; :: thesis: x . j = y . j

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

x . j = y . j by A1;

hence x . j = y . j ; :: thesis: verum