let f be set ; :: thesis: for p being FinSequence holds 1GateCircStr p,f = 1GateCircStr p,f,[p,f]
let p be FinSequence; :: thesis: 1GateCircStr p,f = 1GateCircStr p,f,[p,f]
set S = 1GateCircStr p,f;
A1: the carrier' of (1GateCircStr p,f) = {[p,f]} by Def6;
A2: the Arity of (1GateCircStr p,f) . [p,f] = p by Def6;
A3: the ResultSort of (1GateCircStr p,f) . [p,f] = [p,f] by Def6;
the carrier of (1GateCircStr p,f) = (rng p) \/ {[p,f]} by Def6;
hence 1GateCircStr p,f = 1GateCircStr p,f,[p,f] by A1, A2, A3, Def5; :: thesis: verum