set f = LocSeq (M,S);
set C = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M));
let x1, x2 be object ; FUNCT_1:def 4 ( 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
; 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; verum