deffunc H_{1}( 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_{1}(i,f . i)
from NAT_1:sch 12();

deffunc H_{2}( 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_{2}(j)
from FINSEQ_1:sch 2();

z is FinSequence of BOOLEAN

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

consider f being sequence of BOOLEAN such that

A1: f . 0 = FALSE and

A2: for i being Nat holds f . (i + 1) = H

deffunc H

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

z is FinSequence of BOOLEAN

proof

then reconsider z = z as Tuple of n, BOOLEAN by A3, CARD_1:def 7;
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;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

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