let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S holds FreeGen X is V5()

let X be V5() ManySortedSet of the carrier of S; :: thesis: FreeGen X is V5()

let x be object ; :: according to PBOOLE:def 13 :: thesis: ( not x in the carrier of S or not (FreeGen X) . x is empty )

assume x in the carrier of S ; :: thesis: not (FreeGen X) . x is empty

then reconsider s = x as SortSymbol of S ;

(FreeGen X) . s = FreeGen (s,X) by Def16;

hence not (FreeGen X) . x is empty ; :: thesis: verum

let X be V5() ManySortedSet of the carrier of S; :: thesis: FreeGen X is V5()

let x be object ; :: according to PBOOLE:def 13 :: thesis: ( not x in the carrier of S or not (FreeGen X) . x is empty )

assume x in the carrier of S ; :: thesis: not (FreeGen X) . x is empty

then reconsider s = x as SortSymbol of S ;

(FreeGen X) . s = FreeGen (s,X) by Def16;

hence not (FreeGen X) . x is empty ; :: thesis: verum