set D = DTConOSA X;
let f1, f2 be Element of the carrier of S * ; :: thesis: ( dom f1 = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & f1 . y = LeastSort t ) ) & dom f2 = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & f2 . y = LeastSort t ) ) implies f1 = f2 )
assume that
A6: dom f1 = dom x and
A7: for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & f1 . y = LeastSort t ) and
A8: dom f2 = dom x and
A9: for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & f2 . y = LeastSort t ) ; :: thesis: f1 = f2
for k being Nat st k in dom f1 holds
f1 . k = f2 . k

proof

let k be Nat; :: thesis: ( k in dom f1 implies f1 . k = f2 . k )
assume A10: k in dom f1 ; :: thesis: f1 . k = f2 . k
A11: ex t2 being Element of TS (DTConOSA X) st
( t2 = x . k & f2 . k = LeastSort t2 ) by A6, A9, A10;
ex t1 being Element of TS (DTConOSA X) st
( t1 = x . k & f1 . k = LeastSort t1 ) by A6, A7, A10;
hence f1 . k = f2 . k by A11; :: thesis: verum

end;

hence f1 = f2 by A6, A8, FINSEQ_1:13; :: thesis: verum