let x, y, c be object ; 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)); 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 ; ( a = s . c & b = s . x implies (Following s) . [<*c,x*>,'&'] = a '&' b )
assume A1:
( a = s . c & b = s . x )
; (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
; verum