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

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