let x, y, c be set ; :: thesis: for s being State of (MajorityICirc x,y,c)
for a, b being Element of BOOLEAN st a = s . c & b = s . x holds
(Following s) . [<*c,x*>,'&' ] = a '&' b
set cx = <*c,x*>;
set S3 = 1GateCircStr <*c,x*>,'&' ;
set A3 = 1GateCircuit c,x,'&' ;
set S = MajorityIStr x,y,c;
set A = MajorityICirc x,y,c;
let s be State of (MajorityICirc x,y,c); :: thesis: for a, b being Element of BOOLEAN st a = s . c & b = s . x holds
(Following s) . [<*c,x*>,'&' ] = a '&' b
let a, b be Element of BOOLEAN ; :: thesis: ( a = s . c & b = s . x implies (Following s) . [<*c,x*>,'&' ] = a '&' b )
assume A1: ( a = s . c & b = s . x ) ; :: thesis: (Following s) . [<*c,x*>,'&' ] = a '&' b
reconsider v3 = [<*c,x*>,'&' ] as Element of InnerVertices (1GateCircStr <*c,x*>,'&' ) by Th47;
reconsider v = v3 as Element of InnerVertices (MajorityIStr x,y,c) by Th21;
reconsider s3 = s | the carrier of (1GateCircStr <*c,x*>,'&' ) as State of (1GateCircuit c,x,'&' ) by Th26;
A2: dom s3 = the carrier of (1GateCircStr <*c,x*>,'&' ) by CIRCUIT1:4;
reconsider cc = c, xx = x as Vertex of (1GateCircStr <*c,x*>,'&' ) by Th43;
reconsider cc = cc, xx = xx as Vertex of (MajorityIStr x,y,c) by Th20;
thus (Following s) . [<*c,x*>,'&' ] = (Following s3) . v by CIRCCOMB:72
.= '&' . <*(s3 . cc),(s3 . xx)*> by Th48
.= '&' . <*(s . cc),(s3 . xx)*> by A2, FUNCT_1:70
.= '&' . <*(s . cc),(s . xx)*> by A2, FUNCT_1:70
.= a '&' b by A1, Def6 ; :: thesis: verum