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 SortSymbol of IIG holds size v,A > 0
let A be non-empty finite-yielding MSAlgebra of IIG; :: thesis: for v being SortSymbol of IIG holds size v,A > 0
let v be SortSymbol of IIG; :: thesis: size v,A > 0
consider s being non empty finite Subset of NAT such that
A1: s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } and
A2: size v,A = max s by Def4;
reconsider Y = s as non empty finite real-membered set ;
max Y in { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } by A1, XXREAL_2:def 8;
then consider t being Element of the Sorts of (FreeEnv A) . v such that
A3: card t = max Y ;
size v,A <> 0 by A2, A3;
hence size v,A > 0 ; :: thesis: verum