let f, g be Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN); :: thesis: ( ( for i being Element of 64 -tuples_on BOOLEAN holds f . i = DES-IP i ) & ( for i being Element of 64 -tuples_on BOOLEAN holds g . i = DES-IP i ) implies f = g )
assume AS1: for i being Element of 64 -tuples_on BOOLEAN holds f . i = DES-IP i ; :: thesis: ( ex i being Element of 64 -tuples_on BOOLEAN st not g . i = DES-IP i or f = g )
assume AS2: for i being Element of 64 -tuples_on BOOLEAN holds g . i = DES-IP i ; :: thesis: f = g
L1: ( dom f = 64 -tuples_on BOOLEAN & dom g = 64 -tuples_on BOOLEAN ) by FUNCT_2:def 1;
for i being set st i in 64 -tuples_on BOOLEAN holds
f . i = g . i

proof

let i be set ; :: thesis: ( i in 64 -tuples_on BOOLEAN implies f . i = g . i )
assume i in 64 -tuples_on BOOLEAN ; :: thesis: f . i = g . i
then reconsider i = i as Element of 64 -tuples_on BOOLEAN ;
f . i = DES-IP i by AS1
.= g . i by AS2 ;
hence f . i = g . i ; :: thesis: verum

end;

hence f = g by L1, FUNCT_1:2; :: thesis: verum