let f, g be Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN); ( ( for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . z = DES-F ((z `1),(z `2)) ) & ( for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds g . z = DES-F ((z `1),(z `2)) ) implies f = g )
assume A3:
for i being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . i = DES-F ((i `1),(i `2))
; ( ex z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] st not g . z = DES-F ((z `1),(z `2)) or f = g )
assume A4:
for i being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds g . i = DES-F ((i `1),(i `2))
; f = g
for i being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . i = g . i
hence
f = g
; verum