let x, y, c be object ; :: 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,'&');
reconsider cc = c, xx = x as Vertex of (1GateCircStr (<*c,x*>,'&')) by Th43;
reconsider v3 = [<*c,x*>,'&'] as Element of InnerVertices (1GateCircStr (<*c,x*>,'&')) by Th47;
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 cc = cc, xx = xx as Vertex of (MajorityIStr (x,y,c)) by Th20;
reconsider s3 = s | the carrier of (1GateCircStr (<*c,x*>,'&')) as State of (1GateCircuit (c,x,'&')) by Th26;
reconsider v = v3 as Element of InnerVertices (MajorityIStr (x,y,c)) by Th21;
A2: dom s3 = the carrier of (1GateCircStr (<*c,x*>,'&')) by CIRCUIT1:3;
thus (Following s) . [<*c,x*>,'&'] = (Following s3) . v by CIRCCOMB:64
.= '&' . <*(s3 . cc),(s3 . xx)*> by Th48
.= '&' . <*(s . cc),(s3 . xx)*> by A2, FUNCT_1:47
.= '&' . <*(s . cc),(s . xx)*> by A2, FUNCT_1:47
.= a '&' b by A1, Def5 ; :: thesis: verum