set D = DTConOSA X;
defpred S1[ object , object ] means ex t being Element of TS (DTConOSA X) st
( t = $1 & LeastSort t = $2 );
A1: rng x c= TS (DTConOSA X) by FINSEQ_1:def 4;
A2: for x being object st x in TS (DTConOSA X) holds
ex y being object st
( y in the carrier of S & S1[x,y] )
proof
let x be object ; :: thesis: ( x in TS (DTConOSA X) implies ex y being object st
( y in the carrier of S & S1[x,y] ) )
assume x in TS (DTConOSA X) ; :: thesis: ex y being object st
( y in the carrier of S & S1[x,y] )
then reconsider t = x as Element of TS (DTConOSA X) ;
take LeastSort t ; :: thesis: ( LeastSort t in the carrier of S & S1[x, LeastSort t] )
thus LeastSort t in the carrier of S ; :: thesis: S1[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 object st x in TS (DTConOSA X) holds
S1[x,f . x] from FUNCT_2:sch 1(A2);
 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 FINSEQ_3:120; :: 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 )
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 A4: y in dom x ; :: thesis: ex t being Element of TS (DTConOSA X) st
( t = x . y & (f * x) . y = LeastSort t )
x . y in rng x by A4, FUNCT_1:3;
then reconsider t1 = x . y as Element of TS (DTConOSA X) by A1;
take t1 ; :: thesis: ( t1 = x . y & (f * x) . y = LeastSort t1 )
thus t1 = x . y ; :: thesis: (f * x) . y = LeastSort t1
A5: ex t2 being Element of TS (DTConOSA X) st
( t2 = t1 & LeastSort t2 = f . t1 ) by A3;
y in dom (f * x) by A4, FINSEQ_3:120;
hence (f * x) . y = LeastSort t1 by A5, FINSEQ_3:120; :: thesis: verum