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 ()):] 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 ()):] 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 ()):] c= the carrier of S by A2;
A7: ( i = j1 & p1 = q1 ) by ;
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 ()):] c= the carrier of S by A2, A4;
i = j2 by ;
hence len p1 = len p2 by ; :: 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 ()):] c= the carrier' of S by A3;
A13: ( i = j1 & p1 = q1 ) by ;
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 ()):] c= the carrier' of S by ;
i = j2 by ;
hence len p1 = len p2 by ; :: thesis: verum
end;
end;