defpred S_{1}[ 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_{1}[a,x,z]

for a being Element of BOOLEAN

for x being Element of n -tuples_on BOOLEAN holds S_{1}[a,x,f . (a,x)]
from BINOP_1:sch 3(A1);

hence ex b_{1} 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_{1} . (a,x)) . i = a '&' (x . i)
by BSPACE:3; :: thesis: verum

$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

proof

ex f being Function of [:BOOLEAN,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) st
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_{1}[a,x,z]

let x be Element of n -tuples_on BOOLEAN; :: thesis: ex z being Element of n -tuples_on BOOLEAN st S_{1}[a,x,z]

deffunc H_{1}( 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_{1}(i)
from FUNCT_1:sch 3();

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_{1}[a,x,z]
; :: thesis: verum

end;let x be Element of n -tuples_on BOOLEAN; :: thesis: ex z being Element of n -tuples_on BOOLEAN st S

deffunc H

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

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

y in BOOLEAN

reconsider s = s as boolean-valued Function by A4, TARSKI:def 3, MARGREL1:def 16;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;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

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

for a being Element of BOOLEAN

for x being Element of n -tuples_on BOOLEAN holds S

hence ex b

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