let f be set ; :: thesis: for p, q being FinSequence holds 1GateCircStr p,f tolerates 1GateCircStr q,f
let p, q be FinSequence; :: thesis: 1GateCircStr p,f tolerates 1GateCircStr q,f
set S1 = 1GateCircStr p,f;
set S2 = 1GateCircStr q,f;
A1: ( [p,f] <> [q,f] implies {[p,f]} misses {[q,f]} ) by ZFMISC_1:17;
A2: the Arity of (1GateCircStr q,f) = q,f .--> q by Th47;
the Arity of (1GateCircStr p,f) = p,f .--> p by Th47;
hence the Arity of (1GateCircStr p,f) tolerates the Arity of (1GateCircStr q,f) by A2, A1, Th4, ZFMISC_1:33; :: according to CIRCCOMB:def 1 :: thesis: the ResultSort of (1GateCircStr p,f) tolerates the ResultSort of (1GateCircStr q,f)
A3: the ResultSort of (1GateCircStr q,f) = q,f .--> [q,f] by Th47;
the ResultSort of (1GateCircStr p,f) = p,f .--> [p,f] by Th47;
hence the ResultSort of (1GateCircStr p,f) tolerates the ResultSort of (1GateCircStr q,f) by A3, A1, Th4; :: thesis: verum