set D = DTConOSA X;
defpred S₁[ set , set ] means ex t being Element of TS (DTConOSA X) st
( t = $1 & LeastSort t = $2 );
A1: for x being set st x in TS (DTConOSA X) holds
ex y being set st
( y in the carrier of S & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in TS (DTConOSA X) implies ex y being set st
( y in the carrier of S & S₁[x,y] ) )
assume A2: x in TS (DTConOSA X) ; :: thesis: ex y being set st
( y in the carrier of S & S₁[x,y] )
reconsider t = x as Element of TS (DTConOSA X) by A2;
take LeastSort t ; :: thesis: ( LeastSort t in the carrier of S & S₁[x, LeastSort t] )
thus LeastSort t in the carrier of S ; :: thesis: S₁[x, LeastSort t]
take t ; :: thesis: ( t = x & LeastSort t = LeastSort t )
thus ( t = x & LeastSort t = LeastSort t ) ; :: thesis: verum

end;

consider f being Function of (TS (DTConOSA X)),the carrier of S such that
A3: for x being set st x in TS (DTConOSA X) holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
take f * x ; :: thesis: ( dom (f * x) = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & (f * x) . y = LeastSort t ) ) )
thus dom (f * x) = dom x by ALG_1:1; :: thesis: for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & (f * x) . y = LeastSort t )
A4: rng x c= TS (DTConOSA X) by FINSEQ_1:def 4;
let y be Nat; :: thesis: ( y in dom x implies ex t being Element of TS (DTConOSA X) st
( t = x . y & (f * x) . y = LeastSort t ) )
assume A5: y in dom x ; :: thesis: ex t being Element of TS (DTConOSA X) st
( t = x . y & (f * x) . y = LeastSort t )
A6: y in dom (f * x) by A5, ALG_1:1;
x . y in rng x by A5, FUNCT_1:12;
then reconsider t1 = x . y as Element of TS (DTConOSA X) by A4;
take t1 ; :: thesis: ( t1 = x . y & (f * x) . y = LeastSort t1 )
thus t1 = x . y ; :: thesis: (f * x) . y = LeastSort t1
consider t2 being Element of TS (DTConOSA X) such that
A7: ( t2 = t1 & LeastSort t2 = f . t1 ) by A3;
thus (f * x) . y = LeastSort t1 by A6, A7, ALG_1:1; :: thesis: verum