let f, g be Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN); :: thesis: ( ( 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 AS1: for i being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . i = DES-F ((i `1),(i `2)) ; :: thesis: ( 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 AS2: for i being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds g . i = DES-F ((i `1),(i `2)) ; :: thesis: f = g
for i being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . i = g . i

proof

let i be Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):]; :: thesis: f . i = g . i
thus f . i = DES-F ((i `1),(i `2)) by AS1
.= g . i by AS2 ; :: thesis: verum

end;

hence f = g by FUNCT_2:def 8; :: thesis: verum