set f = LocSeq M,S;
set C = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl M))),(RelIncl M);
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 B4: ( (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, Def4;
A5: card M c= order_type_of (RelIncl M) by CARD_5:51;
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:14;
phi is one-to-one by A7, CARD_5:20;
hence x1 = x2 by A1, A2, A3, B4, A6, A8, A5, FUNCT_1:def 8; :: thesis: verum