defpred S1[ Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)), Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)), Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))] means for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = ($1 . i) . j & keyij = ($2 . i) . j & ($3 . i) . j = Op-XOR (textij,keyij) );
A1: for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[text,key,z]
proof
let text, key be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[text,key,z]
text in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then Q01: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( text = s & len s = 4 ) ;
key in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then Q02: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( key = s & len s = 4 ) ;
defpred S2[ Nat, set ] means ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( $2 = zk & ( for j being Nat st j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . $1) . j & keyij = (key . $1) . j & zk . j = Op-XOR (textij,keyij) ) ) );
Q1: for k being Nat st k in Seg 4 holds
ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk]
proof
let k be Nat; :: thesis: ( k in Seg 4 implies ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk] )
assume Q11: k in Seg 4 ; :: thesis: ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk]
then k in dom text by Q01, FINSEQ_1:def 3;
then text . k in rng text by FUNCT_1:3;
then text . k in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then Q13: ex s being Element of (8 -tuples_on BOOLEAN) * st
( text . k = s & len s = 4 ) ;
then reconsider textk = text . k as Element of (8 -tuples_on BOOLEAN) * ;
k in dom key by Q02, FINSEQ_1:def 3, Q11;
then key . k in rng key by FUNCT_1:3;
then key . k in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then Q16: ex s being Element of (8 -tuples_on BOOLEAN) * st
( key . k = s & len s = 4 ) ;
then reconsider keyk = key . k as Element of (8 -tuples_on BOOLEAN) * ;
defpred S3[ Nat, set ] means ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = textk . $1 & keyij = keyk . $1 & $2 = Op-XOR (textij,keyij) );
Q18: for j being Nat st j in Seg 4 holds
ex xi being Element of 8 -tuples_on BOOLEAN st S3[j,xi]
proof
let j be Nat; :: thesis: ( j in Seg 4 implies ex xi being Element of 8 -tuples_on BOOLEAN st S3[j,xi] )
assume Q19: j in Seg 4 ; :: thesis: ex xi being Element of 8 -tuples_on BOOLEAN st S3[j,xi]
then j in dom textk by Q13, FINSEQ_1:def 3;
then textk . j in rng textk by FUNCT_1:3;
then reconsider textkj = textk . j as Element of 8 -tuples_on BOOLEAN ;
j in dom keyk by Q16, FINSEQ_1:def 3, Q19;
then keyk . j in rng keyk by FUNCT_1:3;
then reconsider keykj = (key . k) . j as Element of 8 -tuples_on BOOLEAN ;
Op-XOR (textkj,keykj) = Op-XOR (textkj,keykj) ;
hence ex xi being Element of 8 -tuples_on BOOLEAN st S3[j,xi] ; :: thesis: verum
end;
consider zk being FinSequence of 8 -tuples_on BOOLEAN such that
Q22: ( dom zk = Seg 4 & ( for j being Nat st j in Seg 4 holds
S3[j,zk . j] ) ) from FINSEQ_1:sch 5(Q18);
 Q23: len zk = 4 by Q22, FINSEQ_1:def 3;
reconsider zk = zk as Element of (8 -tuples_on BOOLEAN) * by FINSEQ_1:def 11;
zk in 4 -tuples_on (8 -tuples_on BOOLEAN) by Q23;
then reconsider zk = zk as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
for j being Nat st j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = textk . j & keyij = keyk . j & zk . j = Op-XOR (textij,keyij) ) by Q22;
hence ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk] ; :: thesis: verum
end;
consider z being FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
Q2: ( dom z = Seg 4 & ( for i being Nat st i in Seg 4 holds
S2[i,z . i] ) ) from FINSEQ_1:sch 5(Q1);
 Q3: len z = 4 by Q2, FINSEQ_1:def 3;
reconsider z = z as Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * by FINSEQ_1:def 11;
z in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by Q3;
then reconsider z = z as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
take z ; :: thesis: S1[text,key,z]
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & (z . i) . j = Op-XOR (textij,keyij) )
proof
let i, j be Nat; :: thesis: ( i in Seg 4 & j in Seg 4 implies ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & (z . i) . j = Op-XOR (textij,keyij) ) )
assume Q4: ( i in Seg 4 & j in Seg 4 ) ; :: thesis: ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & (z . i) . j = Op-XOR (textij,keyij) )
then ex zi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( z . i = zi & ( for j being Nat st j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & zi . j = Op-XOR (textij,keyij) ) ) ) by Q2;
hence ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & (z . i) . j = Op-XOR (textij,keyij) ) by Q4; :: thesis: verum
end;
hence S1[text,key,z] ; :: thesis: verum
end;
consider I being Function of [:(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))):],(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) such that
A2: for x, y being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds S1[x,y,I . (x,y)] from BINOP_1:sch 3(A1);
 take I ; :: thesis: for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((I . (text,key)) . i) . j = Op-XOR (textij,keyij) )
thus for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((I . (text,key)) . i) . j = Op-XOR (textij,keyij) ) by A2; :: thesis: verum