set f = LocSeq (M,S);
set C = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M));
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (LocSeq (M,S)) or not x2 in dom (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 Def1;
then A4: ( (LocSeq (M,S)) . x1 = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . x1 & (LocSeq (M,S)) . x2 = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . x2 ) by A1, Def1;
A5: card M c= order_type_of (RelIncl M) by CARD_5:39;
consider phi being Ordinal-Sequence such that
A6: phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M)) and
A7: phi is increasing and
A8: dom phi = order_type_of (RelIncl M) and
rng phi = M by CARD_5:5;
phi is one-to-one by A7, CARD_5:11;
hence x1 = x2 by A1, A2, A3, A4, A6, A8, A5; :: thesis: verum