let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of the carrier of S
for A being non-empty finite-yielding MSAlgebra of 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 V5() ManySortedSet of the carrier of S; :: thesis: for A being non-empty finite-yielding MSAlgebra of 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 of 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 ) by MCART_1:7; :: thesis: verum