let S be delta-concrete ManySortedSign ; :: thesis: for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds
x is Function
let x be object ; :: thesis: ( x in proj2 ( the carrier of S \/ the carrier' of S) implies x is Function )
consider f being sequence of NAT such that
A1: 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
A2: 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;
set C1 = the carrier of S;
set C2 = the carrier' of S;
assume x in proj2 ( the carrier of S \/ the carrier' of S) ; :: thesis: x is Function
then consider y being object such that
A3: [y,x] in the carrier of S \/ the carrier' of S by XTUPLE_0:def 13;

per cases ( [y,x] in the carrier of S or [y,x] in the carrier' of S ) by XBOOLE_0:def 3, A3;

suppose [y,x] in the carrier of S ; :: thesis: x is Function

then consider i being Element of NAT , p being FinSequence such that
A4: [y,x] = [i,p] and
( len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) by A1;
x = p by A4, XTUPLE_0:1;
hence x is Function ; :: thesis: verum

end;

suppose [y,x] in the carrier' of S ; :: thesis: x is Function

then consider i being Element of NAT , p being FinSequence such that
A5: [y,x] = [i,p] and
( len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) by A2;
x = p by A5, XTUPLE_0:1;
hence x is Function ; :: thesis: verum

end;

end;