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