let f be object ; for p being FinSequence holds
( InputVertices (1GateCircStr (p,f)) = rng p & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )
let p be FinSequence; ( InputVertices (1GateCircStr (p,f)) = rng p & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )
A1:
the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f]
by Th40;
then A2:
rng the ResultSort of (1GateCircStr (p,f)) = {[p,f]}
by FUNCOP_1:8;
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; XBOOLE_0:def 10 ( rng p c= InputVertices (1GateCircStr (p,f)) & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )
A4:
now not [p,f] in rng passume
[p,f] in rng p
;
contradictionthen consider x being
object such that A5:
[x,[p,f]] in p
by XTUPLE_0:def 13;
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, XREGULAR:9;
verum end;
thus
rng p c= InputVertices (1GateCircStr (p,f))
InnerVertices (1GateCircStr (p,f)) = {[p,f]}proof
let x be
object ;
TARSKI:def 3 ( not x in rng p or x in InputVertices (1GateCircStr (p,f)) )
assume A9:
x in rng p
;
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;
verum
end;
thus
InnerVertices (1GateCircStr (p,f)) = {[p,f]}
by A1, FUNCOP_1:8; verum