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 )
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;
A4: x in the carrier of S \/ the carrier' of S by A1, XBOOLE_0:def 3;

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
A5: ( x = [i,p] & len p = f . i ) and
[:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S by A2;
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 A5; :: thesis: rng p c= underlay S
let a be set ; :: 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 A4, A5, Def8; :: 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
A6: ( x = [i,p] & 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 set ; :: 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 A4, A6, Def8; :: thesis: verum

end;

end;