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 Th43; :: 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 Def13;
the Sorts of (1GateCircuit (p,f)) = the carrier of (1GateCircStr (p,f)) --> X by Def13;
hence the Sorts of (1GateCircuit (p,f)) tolerates the Sorts of (1GateCircuit (q,f)) by A1, FUNCOP_1:87; :: 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 Th54;
the Charact of (1GateCircuit (p,f)) = (p,f) .--> f by Th54;
hence the Charact of (1GateCircuit (p,f)) tolerates the Charact of (1GateCircuit (q,f)) by A2, FUNCOP_1:87; :: thesis: verum