let S be delta-concrete ManySortedSign ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( ( ( [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 ) ) ; :: thesis: 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;

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 ; :: thesis: 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; :: thesis: ( ( ( [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 ) ) ; :: thesis: 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;

end;

suppose A4:
( [i,p1] in the carrier of S & [i,p2] in the carrier of S )
; :: thesis: len p1 = len p2

then 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; :: thesis: verum

end;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; :: thesis: verum

suppose A10:
( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S )
; :: thesis: len p1 = len p2

then 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; :: thesis: verum

end;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; :: thesis: verum