let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra of 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 of 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: e in the Sorts of (FreeMSA the Sorts of A) . v ;
A3: FreeMSA the Sorts of A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 16;
A4: (FreeSort the Sorts of A) . v = FreeSort the Sorts of A,v by MSAFREE:def 13;
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 12;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A5: a = e and
A6: ( 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, A3, A4;
thus ex o being OperSymbol of IIG st e . {} = [o,the carrier of IIG] by A1, A5, A6, PRE_CIRC:24; :: thesis: verum