let S be delta-concrete ManySortedSign ; :: thesis: for x being set st ( x in the carrier of S or x in the carrier' of S ) holds
ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
let x be set ; :: thesis: ( ( x in the carrier of S or x in the carrier' of S ) implies ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S ) )
assume A1: ( x in the carrier of S or x in the carrier' of S ) ; :: thesis: ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
A2: x in the carrier of S \/ the carrier' of S by A1, XBOOLE_0:def 3;
consider f being sequence of NAT such that
A3: 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
A4: 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;
A5: for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds
x is Function by Lm3;

per cases ( x in the carrier of S or x in the carrier' of S ) by A1;

suppose x in the carrier of S ; :: thesis: ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )

then consider i being Element of NAT , p being FinSequence such that
A6: x = [i,p] and
len p = f . i and
[:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S by A3;
take i ; :: thesis: ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
take p ; :: thesis: ( x = [i,p] & rng p c= underlay S )
thus x = [i,p] by A6; :: thesis: rng p c= underlay S
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng p or a in underlay S )
thus ( not a in rng p or a in underlay S ) by A2, A6, Def6, A5; :: thesis: verum

end;

suppose x in the carrier' of S ; :: thesis: ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )

then consider i being Element of NAT , p being FinSequence such that
A7: x = [i,p] and
len p = f . i and
[:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S by A4;
take i ; :: thesis: ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
take p ; :: thesis: ( x = [i,p] & rng p c= underlay S )
thus x = [i,p] by A7; :: thesis: rng p c= underlay S
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng p or a in underlay S )
thus ( not a in rng p or a in underlay S ) by A2, A7, Def6, A5; :: thesis: verum

end;

end;