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;

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 ) ; :: 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;

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;

end;