let S be delta-concrete ManySortedSign ; for i being set
for p1, p2 being FinSequence st ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) holds
len p1 = len p2
let i be set ; for p1, p2 being FinSequence st ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) holds
len p1 = len p2
let p1, p2 be FinSequence; ( ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) implies len p1 = len p2 )
assume A1:
( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) )
; len p1 = len p2
consider f being sequence of NAT such that
A2:
for s being object st s in the carrier of S holds
ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S )
and
A3:
for o being object st o in the carrier' of S holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S )
by Def7;
per cases
( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) )
by A1;
suppose A4:
(
[i,p1] in the
carrier of
S &
[i,p2] in the
carrier of
S )
;
len p1 = len p2then consider j1 being
Element of
NAT ,
q1 being
FinSequence such that A5:
[i,p1] = [j1,q1]
and A6:
len q1 = f . j1
and
[:{j1},((f . j1) -tuples_on (underlay S)):] c= the
carrier of
S
by A2;
A7:
(
i = j1 &
p1 = q1 )
by A5, XTUPLE_0:1;
consider j2 being
Element of
NAT ,
q2 being
FinSequence such that A8:
[i,p2] = [j2,q2]
and A9:
len q2 = f . j2
and
[:{j2},((f . j2) -tuples_on (underlay S)):] c= the
carrier of
S
by A2, A4;
i = j2
by A8, XTUPLE_0:1;
hence
len p1 = len p2
by A6, A8, A9, A7, XTUPLE_0:1;
verum end; suppose A10:
(
[i,p1] in the
carrier' of
S &
[i,p2] in the
carrier' of
S )
;
len p1 = len p2then consider j1 being
Element of
NAT ,
q1 being
FinSequence such that A11:
[i,p1] = [j1,q1]
and A12:
len q1 = f . j1
and
[:{j1},((f . j1) -tuples_on (underlay S)):] c= the
carrier' of
S
by A3;
A13:
(
i = j1 &
p1 = q1 )
by A11, XTUPLE_0:1;
consider j2 being
Element of
NAT ,
q2 being
FinSequence such that A14:
[i,p2] = [j2,q2]
and A15:
len q2 = f . j2
and
[:{j2},((f . j2) -tuples_on (underlay S)):] c= the
carrier' of
S
by A3, A10;
i = j2
by A14, XTUPLE_0:1;
hence
len p1 = len p2
by A12, A14, A15, A13, XTUPLE_0:1;
verum end; end;