deffunc H₁( Nat) -> Element of BOOLEAN = ((x /. $1) 'xor' ((Neg2 y) /. $1)) 'xor' ((carry x,(Neg2 y)) /. $1);
consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H₁(j) from FINSEQ_2:sch 1();
A3: dom z = Seg n by A1, FINSEQ_1:def 3;
z is Element of n -tuples_on BOOLEAN by A1, FINSEQ_2:110;
then reconsider z = z as Tuple of n, BOOLEAN by FINSEQ_2:151;
take z ; :: thesis: for i being Nat st i in Seg n holds
z /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i)
let i be Nat; :: thesis: ( i in Seg n implies z /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) )
assume A4: i in Seg n ; :: thesis: z /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i)
A5: i in dom z by A1, A4, FINSEQ_1:def 3;
thus z /. i = z . i by A5, PARTFUN1:def 8
.= ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) by A2, A3, A4 ; :: thesis: verum