A1: ex h being ManySortedSet of NAT st
( 0 -BitMajorityOutput x,y = h . 0 & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput (x . (n + 1)),(y . (n + 1)),z ) ) by Def5;
defpred S₁[ Element of NAT ] means n -BitMajorityOutput x,y is pair ;
A2: S₁[ 0 ] by A1;
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
(n + 1) -BitMajorityOutput x,y = MajorityOutput (x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput x,y) by Th13
.= [<*[<*(x . (n + 1)),(y . (n + 1))*>,'&' ],[<*(y . (n + 1)),(n -BitMajorityOutput x,y)*>,'&' ],[<*(n -BitMajorityOutput x,y),(x . (n + 1))*>,'&' ]*>,or3 ] ;
hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence n -BitMajorityOutput x,y is pair ; :: thesis: verum