defpred S₁[ boolean object , boolean-valued Function, boolean-valued Function] means for i being set st i in Seg n holds
$3 . i = $1 '&' ($2 . i);
A1: for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN ex z being Element of n -tuples_on BOOLEAN st S₁[a,x,z]

proof

let a be Element of BOOLEAN ; :: thesis: for x being Element of n -tuples_on BOOLEAN ex z being Element of n -tuples_on BOOLEAN st S₁[a,x,z]
let x be Element of n -tuples_on BOOLEAN; :: thesis: ex z being Element of n -tuples_on BOOLEAN st S₁[a,x,z]
deffunc H₁( object ) -> object = a '&' (x . $1);
consider s being Function such that
A2: dom s = Seg n and
A3: for i being object st i in Seg n holds
s . i = H₁(i) from FUNCT_1:sch 3();

A4: now :: thesis: for y being object st y in rng s holds
y in BOOLEAN

let y be object ; :: thesis: ( y in rng s implies y in BOOLEAN )
assume y in rng s ; :: thesis: y in BOOLEAN
then consider i being object such that
A5: i in dom s and
A6: y = s . i by FUNCT_1:def 3;
y = a '&' (x . i) by A2, A3, A5, A6;
then ( y = FALSE or y = TRUE ) by XBOOLEAN:def 3;
hence y in BOOLEAN ; :: thesis: verum

end;

reconsider s = s as boolean-valued Function by A4, TARSKI:def 3, MARGREL1:def 16;
s is Function of (Seg n),BOOLEAN by A2, FUNCT_2:2, TARSKI:def 3, A4;
then s is Element of Funcs ((Seg n),BOOLEAN) by FUNCT_2:8;
then reconsider s = s as Element of n -tuples_on BOOLEAN by FINSEQ_2:93;
for i being set st i in Seg n holds
s . i = a '&' (x . i) by A3;
hence ex z being Element of n -tuples_on BOOLEAN st S₁[a,x,z] ; :: thesis: verum

end;

ex f being Function of [:BOOLEAN,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) st
for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN holds S₁[a,x,f . (a,x)] from BINOP_1:sch 3(A1);
hence ex b₁ being Function of [: the carrier of Z_2,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) st
for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(b₁ . (a,x)) . i = a '&' (x . i) by BSPACE:3; :: thesis: verum