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

proof

let a be object ; :: according to FINSEQ_1:def 4,TARSKI:def 3 :: thesis: ( not a in rng z or a in BOOLEAN )
assume a in rng z ; :: thesis: a in BOOLEAN
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: verum

end;

then reconsider z = z as Tuple of n, BOOLEAN by A3, CARD_1:def 7;
take z ; :: thesis: ( z /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
z /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z /. i))) 'or' ((y /. i) '&' (z /. i)) ) )
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: for i being Nat st 1 <= i & i < n holds
z /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z /. i))) 'or' ((y /. i) '&' (z /. i))
let i be Nat; :: thesis: ( 1 <= i & i < n implies z /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z /. i))) 'or' ((y /. i) '&' (z /. i)) )
assume that
A9: 1 <= i and
A10: i < n ; :: thesis: z /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z /. i))) 'or' ((y /. i) '&' (z /. i))
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: verum