let S be delta-concrete ManySortedSign ; :: thesis: for i being set
for p1, p2 being FinSequence st len p2 = len p1 & rng p2 c= underlay S holds
( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) )
let i be set ; :: thesis: for p1, p2 being FinSequence st len p2 = len p1 & rng p2 c= underlay S holds
( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) )
let p1, p2 be FinSequence; :: thesis: ( len p2 = len p1 & rng p2 c= underlay S implies ( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) ) )
assume A1: ( len p2 = len p1 & rng p2 c= underlay S ) ; :: thesis: ( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) )
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;

hereby :: thesis: ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S )

assume [i,p1] in the carrier of S ; :: thesis: [i,p2] in the carrier of S
then consider j1 being Element of NAT , q1 being FinSequence such that
A4: [i,p1] = [j1,q1] and
A5: len q1 = f . j1 and
A6: [:{j1},((f . j1) -tuples_on (underlay S)):] c= the carrier of S by A2;
p1 = q1 by A4, XTUPLE_0:1;
then A7: p2 in (f . j1) -tuples_on (underlay S) by A1, A5, FINSEQ_2:132;
i = j1 by A4, XTUPLE_0:1;
then [i,p2] in [:{j1},((f . j1) -tuples_on (underlay S)):] by A7, ZFMISC_1:105;
hence [i,p2] in the carrier of S by A6; :: thesis: verum

end;

assume [i,p1] in the carrier' of S ; :: thesis: [i,p2] in the carrier' of S
then consider j1 being Element of NAT , q1 being FinSequence such that
A8: [i,p1] = [j1,q1] and
A9: len q1 = f . j1 and
A10: [:{j1},((f . j1) -tuples_on (underlay S)):] c= the carrier' of S by A3;
p1 = q1 by A8, XTUPLE_0:1;
then A11: p2 in (f . j1) -tuples_on (underlay S) by A1, A9, FINSEQ_2:132;
i = j1 by A8, XTUPLE_0:1;
then [i,p2] in [:{j1},((f . j1) -tuples_on (underlay S)):] by A11, ZFMISC_1:105;
hence [i,p2] in the carrier' of S by A10; :: thesis: verum