let S be non void Signature; :: thesis: for X being V5() 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 V5() 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 set such that
A1: x in dom t and
A2: a = t . x by FUNCT_1:def 5;
reconsider x = x as Element of dom t by A1;
a = (t | x) . {} by A2, QC_LANG4:8;
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:23; :: thesis: verum