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} )
( not the carrier' of (1GateCircStr p,f,x) is empty & the ResultSort of (1GateCircStr p,f,x) = p,f .--> x ) by Th43;
then A1: rng the ResultSort of (1GateCircStr p,f,x) = {x} by FUNCOP_1:14;
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