let f be set ; :: thesis: for p being FinSequence holds
( InputVertices (1GateCircStr p,f) = rng p & InnerVertices (1GateCircStr p,f) = {[p,f]} )
let p be FinSequence; :: thesis: ( InputVertices (1GateCircStr p,f) = rng p & InnerVertices (1GateCircStr p,f) = {[p,f]} )
A1: the ResultSort of (1GateCircStr p,f) = p,f .--> [p,f] by Th47;
then A2: rng the ResultSort of (1GateCircStr p,f) = {[p,f]} by FUNCOP_1:14;
A3: the carrier of (1GateCircStr p,f) = (rng p) \/ {[p,f]} by Def6;
hence InputVertices (1GateCircStr p,f) c= rng p by A2, XBOOLE_1:43; :: according to XBOOLE_0:def 10 :: thesis: ( rng p c= InputVertices (1GateCircStr p,f) & InnerVertices (1GateCircStr p,f) = {[p,f]} )

A4: now

assume [p,f] in rng p ; :: thesis: contradiction
then consider x being set such that
A5: [x,[p,f]] in p by RELAT_1:def 5;
A6: {x,[p,f]} in {{x,[p,f]},{x}} by TARSKI:def 2;
A7: {p,f} in {{p,f},{p}} by TARSKI:def 2;
A8: p in {p,f} by TARSKI:def 2;
[p,f] in {x,[p,f]} by TARSKI:def 2;
hence contradiction by A5, A8, A7, A6, ORDINAL1:5; :: thesis: verum

end;

thus rng p c= InputVertices (1GateCircStr p,f) :: thesis: InnerVertices (1GateCircStr p,f) = {[p,f]}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in InputVertices (1GateCircStr p,f) )
assume A9: x in rng p ; :: thesis: x in InputVertices (1GateCircStr p,f)
then A10: x in (rng p) \/ {[p,f]} by XBOOLE_0:def 3;
not x in {[p,f]} by A4, A9, TARSKI:def 1;
hence x in InputVertices (1GateCircStr p,f) by A2, A3, A10, XBOOLE_0:def 5; :: thesis: verum

end;

thus InnerVertices (1GateCircStr p,f) = {[p,f]} by A1, FUNCOP_1:14; :: thesis: verum