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 hence f1 = f2 by A6, A8, FINSEQ_1:13; :: thesis: verum