let x, y, c be set ; :: thesis: for s being State of (BorrowICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,and2] = a '&' b
set xy = <*x,y*>;
set yc = <*y,c*>;
set xc = <*x,c*>;
set S1 = 1GateCircStr (<*x,y*>,and2a);
set A1 = 1GateCircuit (x,y,and2a);
set S2 = 1GateCircStr (<*y,c*>,and2);
set A2 = 1GateCircuit (y,c,and2);
set S3 = 1GateCircStr (<*x,c*>,and2a);
set A3 = 1GateCircuit (x,c,and2a);
set S = BorrowIStr (x,y,c);
set A = BorrowICirc (x,y,c);
set v2 = [<*y,c*>,and2];
let s be State of (BorrowICirc (x,y,c)); :: thesis: for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,and2] = a '&' b
let a, b be Element of BOOLEAN ; :: thesis: ( a = s . y & b = s . c implies (Following s) . [<*y,c*>,and2] = a '&' b )
assume A1: ( a = s . y & b = s . c ) ; :: thesis: (Following s) . [<*y,c*>,and2] = a '&' b
reconsider yy = y, cc = c as Vertex of (1GateCircStr (<*y,c*>,and2)) by FACIRC_1:43;
reconsider v2 = [<*y,c*>,and2] as Element of InnerVertices (1GateCircStr (<*y,c*>,and2)) by FACIRC_1:47;
A2: (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) = (1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,y*>,and2a)) by FACIRC_1:23;
then A3: BorrowIStr (x,y,c) = (1GateCircStr (<*y,c*>,and2)) +* ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*x,c*>,and2a))) by CIRCCOMB:6;
then reconsider v = v2 as Element of InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21;
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) = (1GateCircuit (y,c,and2)) +* (1GateCircuit (x,y,and2a)) by FACIRC_1:24;
then A4: BorrowICirc (x,y,c) = (1GateCircuit (y,c,and2)) +* ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (x,c,and2a))) by A2, FACIRC_1:25;
then reconsider s2 = s | the carrier of (1GateCircStr (<*y,c*>,and2)) as State of (1GateCircuit (y,c,and2)) by FACIRC_1:26;
reconsider yy = yy, cc = cc as Vertex of (BorrowIStr (x,y,c)) by A3, FACIRC_1:20;
A5: dom s2 = the carrier of (1GateCircStr (<*y,c*>,and2)) by CIRCUIT1:3;
thus (Following s) . [<*y,c*>,and2] = (Following s2) . v by A3, A4, CIRCCOMB:64
.= and2 . <*(s2 . yy),(s2 . cc)*> by FACIRC_1:50
.= and2 . <*(s . yy),(s2 . cc)*> by A5, FUNCT_1:47
.= and2 . <*(s . yy),(s . cc)*> by A5, FUNCT_1:47
.= a '&' b by A1, FACIRC_1:def 6 ; :: thesis: verum