deffunc H₁( set ) -> Element of BOOLEAN = (p /. $1) '&' (q /. $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 in BOOLEAN * by FINSEQ_1:def 11;
then z in n -tuples_on BOOLEAN by A1;
then reconsider z = z as Element of n -tuples_on BOOLEAN ;
take z ; :: thesis: for i being set st i in Seg n holds
z . i = (p /. i) '&' (q /. i)
let i be set ; :: thesis: ( i in Seg n implies z . i = (p /. i) '&' (q /. i) )
assume i in Seg n ; :: thesis: z . i = (p /. i) '&' (q /. i)
hence z . i = (p /. i) '&' (q /. i) by A2, A3; :: thesis: verum