let f be set ; for p, q being FinSequence holds 1GateCircStr (p,f) tolerates 1GateCircStr (q,f)
let p, q be FinSequence; 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:11;
A2:
the Arity of (1GateCircStr (q,f)) = (q,f) .--> q
by Th40;
the Arity of (1GateCircStr (p,f)) = (p,f) .--> p
by Th40;
hence
the Arity of (1GateCircStr (p,f)) tolerates the Arity of (1GateCircStr (q,f))
by A2, A1, XTUPLE_0:1; CIRCCOMB:def 1 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 Th40;
the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f]
by Th40;
hence
the ResultSort of (1GateCircStr (p,f)) tolerates the ResultSort of (1GateCircStr (q,f))
by A3, A1; verum