let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let A be non-empty finite-yielding MSAlgebra over S; :: thesis: for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let V be Variables of A; :: thesis: for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let X be SetWithCompoundTerm of S,V; :: thesis: for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let G be non empty non void Circuit-like ManySortedSign ; :: thesis: for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let C be non-empty Circuit of G; :: thesis: ( X,A specifies C implies C calculates X,A )
given f, g being Function such that A1: C,X -Circuit A are_similar_wrt f,g ; :: according to CIRCTRM1:def 14,CIRCTRM1:def 16 :: thesis: C calculates X,A
take f " ; :: according to CIRCTRM1:def 15 :: thesis: ex g being Function st
( f " ,g form_embedding_of X -Circuit A,C & f " preserves_inputs_of X -CircuitStr ,G )
take g " ; :: thesis: ( f " ,g " form_embedding_of X -Circuit A,C & f " preserves_inputs_of X -CircuitStr ,G )
thus f " ,g " form_embedding_of X -Circuit A,C by A1; :: thesis: f " preserves_inputs_of X -CircuitStr ,G
X -Circuit A,C are_similar_wrt f " ,g " by A1, Th39;
hence f " preserves_inputs_of X -CircuitStr ,G by Th53; :: thesis: verum