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 n 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 n 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 n holds 1GateCircuit p,f tolerates 1GateCircuit q,f
let p, q be FinSeqLen of n; :: thesis: 1GateCircuit p,f tolerates 1GateCircuit q,f
set S1 = 1GateCircStr p,f;
set S2 = 1GateCircStr q,f;
set A1 = 1GateCircuit p,f;
set A2 = 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) )
A1: the Sorts of (1GateCircuit q,f) = the carrier of (1GateCircStr q,f) --> X by Def14;
the Sorts of (1GateCircuit p,f) = the carrier of (1GateCircStr p,f) --> X by Def14;
hence the Sorts of (1GateCircuit p,f) tolerates the Sorts of (1GateCircuit q,f) by A1, Th4; :: thesis: the Charact of (1GateCircuit p,f) tolerates the Charact of (1GateCircuit q,f)
A2: the Charact of (1GateCircuit q,f) = q,f .--> f by Th62;
the Charact of (1GateCircuit p,f) = p,f .--> f by Th62;
hence the Charact of (1GateCircuit p,f) tolerates the Charact of (1GateCircuit q,f) by A2, Th4; :: thesis: verum