let n be Nat; :: thesis: for X being non empty set
for f being Function of (n -tuples_on X),X
for p, q being FinSeqLen of holds 1GateCircuit p,f tolerates 1GateCircuit q,f
let X be non empty set ; :: thesis: for f being Function of (n -tuples_on X),X
for p, q being FinSeqLen of holds 1GateCircuit p,f tolerates 1GateCircuit q,f
let f be Function of (n -tuples_on X),X; :: thesis: for p, q being FinSeqLen of holds 1GateCircuit p,f tolerates 1GateCircuit q,f
let p, q be FinSeqLen of ; :: thesis: 1GateCircuit p,f tolerates 1GateCircuit q,f
thus 1GateCircStr p,f tolerates 1GateCircStr q,f by Th51; :: according to CIRCCOMB:def 3 :: thesis: ( the Sorts of (1GateCircuit p,f) tolerates the Sorts of (1GateCircuit q,f) & the Charact of (1GateCircuit p,f) tolerates the Charact of (1GateCircuit q,f) )
set S1 = 1GateCircStr p,f;
set S2 = 1GateCircStr q,f;
set A1 = 1GateCircuit p,f;
set A2 = 1GateCircuit q,f;
( the Sorts of (1GateCircuit p,f) = the carrier of (1GateCircStr p,f) --> X & the Sorts of (1GateCircuit q,f) = the carrier of (1GateCircStr q,f) --> X ) by Def14;
hence the Sorts of (1GateCircuit p,f) tolerates the Sorts of (1GateCircuit q,f) by Th4; :: thesis: the Charact of (1GateCircuit p,f) tolerates the Charact of (1GateCircuit q,f)
( the Charact of (1GateCircuit p,f) = p,f .--> f & the Charact of (1GateCircuit q,f) = q,f .--> f ) by Th62;
hence the Charact of (1GateCircuit p,f) tolerates the Charact of (1GateCircuit q,f) by Th4; :: thesis: verum