let f, x be set ; :: thesis: for p being FinSequence holds
( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} )
let p be FinSequence; :: thesis: ( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} )
the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x by Th36;
then A1: rng the ResultSort of (1GateCircStr (p,f,x)) = {x} by FUNCOP_1:8;
the carrier of (1GateCircStr (p,f,x)) = (rng p) \/ {x} by Def5;
hence ( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} ) by A1, XBOOLE_1:40; :: thesis: verum