let S be non empty non void ManySortedSign ; :: thesis: for V being V2() ManySortedSet of the carrier of S holds S -Terms V = Union (FreeSort V)
let V be V2() ManySortedSet of the carrier of S; :: thesis: S -Terms V = Union (FreeSort V)
set T = S -Terms V;
set X = V;
A1: dom (FreeSort V) = the carrier of S by PARTFUN1:def 2;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Union (FreeSort V) c= S -Terms V
let x be object ; :: thesis: ( x in S -Terms V implies x in Union (FreeSort V) )
assume x in S -Terms V ; :: thesis: x in Union (FreeSort V)
then reconsider t = x as Term of S,V ;
consider s being SortSymbol of S such that
A2: t in FreeSort (V,s) by Th11;
FreeSort (V,s) = (FreeSort V) . s by MSAFREE:def 11;
hence x in Union (FreeSort V) by A1, A2, CARD_5:2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (FreeSort V) or x in S -Terms V )
assume x in Union (FreeSort V) ; :: thesis: x in S -Terms V
then consider y being object such that
A3: y in dom (FreeSort V) and
A4: x in (FreeSort V) . y by CARD_5:2;
reconsider y = y as SortSymbol of S by A3, PARTFUN1:def 2;
x in FreeSort (V,y) by A4, MSAFREE:def 11;
hence x in S -Terms V ; :: thesis: verum