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