set X = LocNums M,S;
set f = LocSeq M,S;
set C = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S));
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 (LocSeq M,S) or not x2 in proj1 (LocSeq M,S) or not (LocSeq M,S) . x1 = (LocSeq M,S) . x2 or x1 = x2 )
assume that
A1: ( x1 in dom (LocSeq M,S) & x2 in dom (LocSeq M,S) ) and
A2: (LocSeq M,S) . x1 = (LocSeq M,S) . x2 ; :: thesis: x1 = x2
A3: dom (LocSeq M,S) = card M by Def4;
then ( (LocSeq M,S) . x1 = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . x1) & (LocSeq M,S) . x2 = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . x2) ) by A1, Def4;
then A4: (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . x1 = (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . x2 by A2, AMISTD_1:25;
A5: card M c= order_type_of (RelIncl (LocNums M,S)) by Th28;
consider phi being Ordinal-Sequence such that
A6: phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S)) and
A7: phi is increasing and
A8: dom phi = order_type_of (RelIncl (LocNums M,S)) and
rng phi = LocNums M,S by CARD_5:14;
phi is one-to-one by A7, CARD_5:20;
hence x1 = x2 by A1, A3, A4, A6, A8, A5, FUNCT_1:def 8; :: thesis: verum