let f be object ; :: 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 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; :: according to XBOOLE_0:def 10 :: thesis: ( rng p c= InputVertices (1GateCircStr (p,f)) & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )
A4: now :: thesis: not [p,f] in rng p
assume [p,f] in rng p ; :: thesis: contradiction
then 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; :: thesis: verum
end;
thus rng p c= InputVertices (1GateCircStr (p,f)) :: thesis: InnerVertices (1GateCircStr (p,f)) = {[p,f]}
proof
let x be object ; :: 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:8; :: thesis: verum