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: ( the Arity of (1GateCircStr p,f) = p,f .--> p & the Arity of (1GateCircStr q,f) = q,f .--> q ) by Th47;
A2: ( the ResultSort of (1GateCircStr p,f) = p,f .--> [p,f] & the ResultSort of (1GateCircStr q,f) = q,f .--> [q,f] ) by Th47;
A3: ( [p,f] <> [q,f] implies {[p,f]} misses {[q,f]} ) by ZFMISC_1:17;
hence the Arity of (1GateCircStr p,f) tolerates the Arity of (1GateCircStr q,f) by A1, Th4, ZFMISC_1:33; :: according to CIRCCOMB:def 1 :: thesis: the ResultSort of (1GateCircStr p,f) tolerates the ResultSort of (1GateCircStr q,f)
thus the ResultSort of (1GateCircStr p,f) tolerates the ResultSort of (1GateCircStr q,f) by A2, A3, Th4; :: thesis: verum