let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra of S holds X1 -Circuit A tolerates X2 -Circuit A
let V be V5() ManySortedSet of the carrier of S; :: thesis: for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra of S holds X1 -Circuit A tolerates X2 -Circuit A
let X1, X2 be SetWithCompoundTerm of S,V; :: thesis: for A being non-empty MSAlgebra of S holds X1 -Circuit A tolerates X2 -Circuit A
let A be non-empty MSAlgebra of S; :: thesis: X1 -Circuit A tolerates X2 -Circuit A
thus ( the Arity of (X1 -CircuitStr ) tolerates the Arity of (X2 -CircuitStr ) & the ResultSort of (X1 -CircuitStr ) tolerates the ResultSort of (X2 -CircuitStr ) ) by Th7; :: according to CIRCCOMB:def 1,CIRCCOMB:def 3 :: thesis: ( the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) & the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A) )
thus the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) :: thesis: the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A)

proof

let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (proj1 the Sorts of (X1 -Circuit A)) /\ (proj1 the Sorts of (X2 -Circuit A)) or the Sorts of (X1 -Circuit A) . x = the Sorts of (X2 -Circuit A) . x )
assume A1: x in (dom the Sorts of (X1 -Circuit A)) /\ (dom the Sorts of (X2 -Circuit A)) ; :: thesis: the Sorts of (X1 -Circuit A) . x = the Sorts of (X2 -Circuit A) . x
then A2: x in dom the Sorts of (X1 -Circuit A) by XBOOLE_0:def 4;
A3: x in dom the Sorts of (X2 -Circuit A) by A1, XBOOLE_0:def 4;
A4: x in the carrier of (X1 -CircuitStr ) by A2, PARTFUN1:def 4;
reconsider v1 = x as Vertex of (X1 -CircuitStr ) by A2, PARTFUN1:def 4;
reconsider v2 = x as Vertex of (X2 -CircuitStr ) by A3, PARTFUN1:def 4;
reconsider t = x as Term of S,V by A4, Th4;
thus the Sorts of (X1 -Circuit A) . x = the_sort_of v1,A by Def4
.= the Sorts of A . (the_sort_of t) by Def2
.= the_sort_of v2,A by Def2
.= the Sorts of (X2 -Circuit A) . x by Def4 ; :: thesis: verum

end;

let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (proj1 the Charact of (X1 -Circuit A)) /\ (proj1 the Charact of (X2 -Circuit A)) or the Charact of (X1 -Circuit A) . x = the Charact of (X2 -Circuit A) . x )
assume A5: x in (dom the Charact of (X1 -Circuit A)) /\ (dom the Charact of (X2 -Circuit A)) ; :: thesis: the Charact of (X1 -Circuit A) . x = the Charact of (X2 -Circuit A) . x
then A6: x in dom the Charact of (X1 -Circuit A) by XBOOLE_0:def 4;
A7: x in dom the Charact of (X2 -Circuit A) by A5, XBOOLE_0:def 4;
reconsider g1 = x as Gate of (X1 -CircuitStr ) by A6, PARTFUN1:def 4;
reconsider g2 = x as Gate of (X2 -CircuitStr ) by A7, PARTFUN1:def 4;
thus the Charact of (X1 -Circuit A) . x = the_action_of g1,A by Def5
.= the Charact of A . ((g1 . {} ) `1 ) by Def3
.= the_action_of g2,A by Def3
.= the Charact of (X2 -Circuit A) . x by Def5 ; :: thesis: verum