consider s being object such that

A1: s in the carrier of S and

A2: not X . s is empty by PBOOLE:def 12;

reconsider s = s as SortSymbol of S by A1;

set x = the Element of X . s;

root-tree [ the Element of X . s,s] in the Sorts of (Free (S,X)) . s by A2, Th4;

hence the Sorts of (Free (S,X)) is V9() ; :: according to CATALG_1:def 2 :: thesis: verum

A1: s in the carrier of S and

A2: not X . s is empty by PBOOLE:def 12;

reconsider s = s as SortSymbol of S by A1;

set x = the Element of X . s;

root-tree [ the Element of X . s,s] in the Sorts of (Free (S,X)) . s by A2, Th4;

hence the Sorts of (Free (S,X)) is V9() ; :: according to CATALG_1:def 2 :: thesis: verum