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 Function of NAT , NAT such that
A2: for s being set 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 set 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 Def9;

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] & len q1 = f . j1 ) and
A5: [:{j1},((f . j1) -tuples_on (underlay S)):] c= the carrier of S by A2;
A6: ( i = j1 & p1 = q1 ) by A4, ZFMISC_1:33;
then p2 in (f . j1) -tuples_on (underlay S) by A1, A4, Th4;
then [i,p2] in [:{j1},((f . j1) -tuples_on (underlay S)):] by A6, ZFMISC_1:128;
hence [i,p2] in the carrier of S by A5; :: 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
A7: ( [i,p1] = [j1,q1] & len q1 = f . j1 ) and
A8: [:{j1},((f . j1) -tuples_on (underlay S)):] c= the carrier' of S by A3;
A9: ( i = j1 & p1 = q1 ) by A7, ZFMISC_1:33;
then p2 in (f . j1) -tuples_on (underlay S) by A1, A7, Th4;
then [i,p2] in [:{j1},((f . j1) -tuples_on (underlay S)):] by A9, ZFMISC_1:128;
hence [i,p2] in the carrier' of S by A8; :: thesis: verum