deffunc H₁( Nat, Element of BOOLEAN ) -> Element of BOOLEAN = (((x /. ($1 + 1)) '&' (y /. ($1 + 1))) 'or' ((x /. ($1 + 1)) '&' $2)) 'or' ((y /. ($1 + 1)) '&' $2);
consider f being sequence of BOOLEAN such that
A1: f . 0 = FALSE and
A2: for i being Nat holds f . (i + 1) = H₁(i,f . i) from NAT_1:sch 12();
deffunc H₂( Nat) -> set = f . ($1 - 1);
consider z being FinSequence such that
A3: len z = n and
A4: for j being Nat st j in dom z holds
z . j = H₂(j) from FINSEQ_1:sch 2();
z is FinSequence of BOOLEAN

let a be object ; :: according to FINSEQ_1:def 4,TARSKI:def 3 :: thesis:
assume a in rng z ; :: thesis:
then consider b being object such that
A5: b in dom z and
A6: a = z . b by FUNCT_1:def 3;
A7: b in Seg n by A3, A5, FINSEQ_1:def 3;
reconsider b = b as Element of NAT by A5;
b >= 1 by A7, FINSEQ_1:1;
then reconsider c = b - 1 as Element of NAT by INT_1:5;
z . b = f . c by A4, A5;
hence a in BOOLEAN by A6; :: thesis:

end;

then reconsider z = z as Tuple of n, BOOLEAN by A3, CARD_1:def 7;
take z ; :: thesis:
0 + 1 <= n by NAT_1:13;
then 1 in Seg n ;
then A8: 1 in dom z by A3, FINSEQ_1:def 3;
hence z /. 1 = z . 1 by PARTFUN1:def 6
.= f . (1 - 1) by A4, A8
.= FALSE by A1 ;
:: thesis:
let i be Nat; :: thesis:
assume that
A9: 1 <= i and
A10: i < n ; :: thesis:
consider j being Nat such that
A11: j + 1 = i by A9, NAT_1:6;
j + 1 in Seg n by A9, A10, A11;
then A12: j + 1 in dom z by A3, FINSEQ_1:def 3;
then A13: z /. (j + 1) = z . (j + 1) by PARTFUN1:def 6
.= f . ((j + 1) - 1) by A4, A12
.= f . j ;
A14: (i + 1) - 1 = i ;
( 1 <= i + 1 & i + 1 <= n ) by A9, A10, NAT_1:13;
then A15: i + 1 in dom z by A3, FINSEQ_3:25;
hence z /. (i + 1) = z . (i + 1) by PARTFUN1:def 6
.= f . (j + 1) by A4, A11, A14, A15
.= (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z /. i))) 'or' ((y /. i) '&' (z /. i)) by A2, A11, A13 ;
:: thesis: