defpred S1[ 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 S1[a,x,z]
proof
let a be
Element of
BOOLEAN ;
for x being Element of n -tuples_on BOOLEAN ex z being Element of n -tuples_on BOOLEAN st S1[a,x,z]let x be
Element of
n -tuples_on BOOLEAN;
ex z being Element of n -tuples_on BOOLEAN st S1[a,x,z]
deffunc H1(
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 = H1(
i)
from FUNCT_1:sch 3();
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
S1[
a,
x,
z]
;
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 S1[a,x,f . (a,x)]
from BINOP_1:sch 3(A1);
hence
ex b1 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
(b1 . (a,x)) . i = a '&' (x . i)
by BSPACE:3; verum