defpred S1[ Nat, set ] means ex si, ti being Element of n -tuples_on BOOLEAN st
( si = s . $1 & ti = t . $1 & $2 = Op-XOR (si,ti) );
P1: for k being Nat st k in Seg m holds
ex z being Element of n -tuples_on BOOLEAN st S1[k,z]
proof
let k be Nat; :: thesis: ( k in Seg m implies ex z being Element of n -tuples_on BOOLEAN st S1[k,z] )
assume AS: k in Seg m ; :: thesis: ex z being Element of n -tuples_on BOOLEAN st S1[k,z]
s in m -tuples_on (n -tuples_on BOOLEAN) ;
then ex v being Element of (n -tuples_on BOOLEAN) * st
( s = v & len v = m ) ;
then k in dom s by FINSEQ_1:def 3, AS;
then s . k in rng s by FUNCT_1:3;
then reconsider sk = s . k as Element of n -tuples_on BOOLEAN ;
t in m -tuples_on (n -tuples_on BOOLEAN) ;
then ex v being Element of (n -tuples_on BOOLEAN) * st
( t = v & len v = m ) ;
then k in dom t by FINSEQ_1:def 3, AS;
then t . k in rng t by FUNCT_1:3;
then reconsider tk = t . k as Element of n -tuples_on BOOLEAN ;
Op-XOR (sk,tk) is Element of n -tuples_on BOOLEAN ;
hence ex z being Element of n -tuples_on BOOLEAN st S1[k,z] ; :: thesis: verum
end;
consider p being FinSequence of n -tuples_on BOOLEAN such that
P3: ( dom p = Seg m & ( for k being Nat st k in Seg m holds
S1[k,p . k] ) ) from FINSEQ_1:sch 5(P1);
 P4: len p = m by P3, FINSEQ_1:def 3;
p in (n -tuples_on BOOLEAN) * by FINSEQ_1:def 11;
then p in m -tuples_on (n -tuples_on BOOLEAN) by P4;
then reconsider p = p as Element of m -tuples_on (n -tuples_on BOOLEAN) ;
take p ; :: thesis: for i being Element of Seg m holds p . i = Op-XOR ((s . i),(t . i))
now :: thesis: for i being Element of Seg m holds p . i = Op-XOR ((s . i),(t . i))
let i be Element of Seg m; :: thesis: p . i = Op-XOR ((s . i),(t . i))
ex si, ti being Element of n -tuples_on BOOLEAN st
( si = s . i & ti = t . i & p . i = Op-XOR (si,ti) ) by P3;
hence p . i = Op-XOR ((s . i),(t . i)) ; :: thesis: verum
end;
hence for i being Element of Seg m holds p . i = Op-XOR ((s . i),(t . i)) ; :: thesis: verum