deffunc H1( Tuple of 3,BOOLEAN ) -> Element of BOOLEAN = F1(($1 . 1),($1 . 2),($1 . 3));
consider f being Function of (3 -tuples_on BOOLEAN ),BOOLEAN such that
A1:
for a being Tuple of 3,BOOLEAN holds f . a = H1(a)
from FUNCT_2:sch 4();
hereby :: thesis: verum
take f =
f;
:: thesis: for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F1(x,y,z)let x,
y,
z be
Element of
BOOLEAN ;
:: thesis: f . <*x,y,z*> = F1(x,y,z)reconsider a =
<*x,y,z*> as
Tuple of 3,
BOOLEAN by FINSEQ_2:124;
thus f . <*x,y,z*> =
F1(
(a . 1),
(a . 2),
(a . 3))
by A1
.=
F1(
x,
(a . 2),
(a . 3))
by FINSEQ_1:62
.=
F1(
x,
y,
(a . 3))
by FINSEQ_1:62
.=
F1(
x,
y,
z)
by FINSEQ_1:62
;
:: thesis: verum
end;