let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra over IIG
for v being Element of IIG
for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
let A be non-empty finite-yielding MSAlgebra over IIG; :: thesis: for v being Element of IIG
for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
let v be Element of IIG; :: thesis: for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
let e be Element of the Sorts of (FreeEnv A) . v; :: thesis: ( 1 < card e implies ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG] )
set X = the Sorts of A;
assume A1: 1 < card e ; :: thesis: ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
A2: ( (FreeSort the Sorts of A) . v = FreeSort ( the Sorts of A,v) & FreeSort ( the Sorts of A,v) = { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) } ) by MSAFREE:def 10, MSAFREE:def 11;
( e in the Sorts of (FreeMSA the Sorts of A) . v & FreeMSA the Sorts of A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) ) by MSAFREE:def 14;
then ex a being Element of TS (DTConMSA the Sorts of A) st
( a = e & ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) ) by A2;
hence ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG] by A1, PRE_CIRC:19; :: thesis: verum