let F1, F2 be 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))); :: 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 & ((F1 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ) & ( 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 & ((F2 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ) implies F1 = F2 )
assume A1: 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 & ((F1 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ; :: thesis: ( ex text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & ( for textij, keyij being Element of 8 -tuples_on BOOLEAN holds
( not textij = (text . i) . j or not keyij = (key . i) . j or not ((F2 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ) ) or F1 = F2 )
assume A2: 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 & ((F2 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ; :: thesis: F1 = F2
now :: thesis: for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds F1 . (text,key) = F2 . (text,key)
let text, key be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: F1 . (text,key) = F2 . (text,key)
now :: thesis: for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((F1 . (text,key)) . i) . j = ((F2 . (text,key)) . i) . j
let i, j be Nat; :: thesis: ( i in Seg 4 & j in Seg 4 implies ((F1 . (text,key)) . i) . j = ((F2 . (text,key)) . i) . j )
assume A3: ( i in Seg 4 & j in Seg 4 ) ; :: thesis: ((F1 . (text,key)) . i) . j = ((F2 . (text,key)) . i) . j
then A4: ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((F1 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) by A1;
A5: ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((F2 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) by A3, A2;
thus ((F1 . (text,key)) . i) . j = ((F2 . (text,key)) . i) . j by A4, A5; :: thesis: verum
end;
hence F1 . (text,key) = F2 . (text,key) by LM01; :: thesis: verum
end;
hence F1 = F2 by BINOP_1:2; :: thesis: verum