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