let S be non void Signature; :: thesis: for X being V8() 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 V8() 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

for t being Term of S,X

for a being Element of rng t holds a = [(a `1),(a `2)]

let X be V8() 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