let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for A being non-empty finite-yielding MSAlgebra over S
for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for A being non-empty finite-yielding MSAlgebra over S
for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding
let A be non-empty finite-yielding MSAlgebra over S; :: thesis: for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding
let t be non empty Subset of (S -Terms V); :: thesis: t -Circuit A is finite-yielding
let i be object ; :: according to MSAFREE2:def 11,FINSET_1:def 5 :: thesis: ( not i in the carrier of (t -CircuitStr) or the Sorts of (t -Circuit A) . i is finite )
assume i in the carrier of (t -CircuitStr) ; :: thesis: the Sorts of (t -Circuit A) . i is finite
then reconsider i = i as Vertex of (t -CircuitStr) ;
reconsider u = i as Term of S,V by Th4;
A1: the Sorts of A is finite-yielding by MSAFREE2:def 11;
the Sorts of (t -Circuit A) . i = the_sort_of (i,A) by Def4
.= the Sorts of A . (the_sort_of u) by Def2 ;
hence the Sorts of (t -Circuit A) . i is finite by A1; :: thesis: verum