let S be non void Signature; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Term of S,X
for a being Element of rng t holds a = [(a `1),(a `2)]
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Term of S,X
for a being Element of rng t holds a = [(a `1),(a `2)]
let t be Term of S,X; :: thesis: for a being Element of rng t holds a = [(a `1),(a `2)]
let a be Element of rng t; :: thesis: a = [(a `1),(a `2)]
consider x being object such that
A1: x in dom t and
A2: a = t . x by FUNCT_1:def 3;
reconsider x = x as Element of dom t by A1;
a = (t | x) . {} by A2, TREES_9:35;
then ( ex s being SortSymbol of S ex v being Element of X . s st a = [v,s] or a in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2;
hence a = [(a `1),(a `2)] by MCART_1:21; :: thesis: verum