let S be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; :: thesis: for A being non-empty gate`2=den Boolean Circuit of S st [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices S holds
for s being State of A holds (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE
let A be non-empty gate`2=den Boolean Circuit of S; :: thesis: ( [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices S implies for s being State of A holds (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE )
set f0 = (0 -tuples_on BOOLEAN) --> FALSE;
assume [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices S ; :: thesis: for s being State of A holds (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE
then A1: [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in the carrier' of S by FACIRC_1:37;
let s be State of A; :: thesis: (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE
A2: (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = ((0 -tuples_on BOOLEAN) --> FALSE) . (s * <*>) by A1, FACIRC_1:35;

per cases ( s * <*> in dom ((0 -tuples_on BOOLEAN) --> FALSE) or not s * <*> in dom ((0 -tuples_on BOOLEAN) --> FALSE) ) ;

suppose A3: s * <*> in dom ((0 -tuples_on BOOLEAN) --> FALSE) ; :: thesis: (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE

dom ((0 -tuples_on BOOLEAN) --> FALSE) = 0 -tuples_on BOOLEAN by FUNCOP_1:13;
hence (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE by A2, FUNCOP_1:7, A3; :: thesis: verum

end;

suppose not s * <*> in dom ((0 -tuples_on BOOLEAN) --> FALSE) ; :: thesis: (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE

hence (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE by A2, XBOOLEAN:def 1, FUNCT_1:def 2; :: thesis: verum

end;

end;