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

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