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 SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
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 SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let A be non-empty finite-yielding MSAlgebra over S; :: thesis: for X being SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let X be SetWithCompoundTerm of S,V; :: thesis: for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let g be OperSymbol of (X -CircuitStr); :: thesis: for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let o be OperSymbol of S; :: thesis: ( g . {} = [o, the carrier of S] implies Den (g,(X -Circuit A)) = Den (o,A) )
Den (g,(X -Circuit A)) = the_action_of (g,A) by Def5
.= the Charact of A . ((g . {}) `1) by Def3 ;
hence ( g . {} = [o, the carrier of S] implies Den (g,(X -Circuit A)) = Den (o,A) ) ; :: thesis: verum