L1: dom (DES-PIPINV * DES-PIP) = 64 -tuples_on BOOLEAN by FUNCT_2:def 1;
for x being set st x in 64 -tuples_on BOOLEAN holds
(DES-PIPINV * DES-PIP) . x = x

proof

let x be set ; :: thesis: ( x in 64 -tuples_on BOOLEAN implies (DES-PIPINV * DES-PIP) . x = x )
assume x in 64 -tuples_on BOOLEAN ; :: thesis: (DES-PIPINV * DES-PIP) . x = x
then reconsider x = x as Element of 64 -tuples_on BOOLEAN ;
(DES-PIPINV * DES-PIP) . x = DES-PIPINV . (DES-PIP . x) by FUNCT_2:15
.= DES-PIPINV . (DES-IP x) by defPIP
.= DES-IPINV (DES-IP x) by defPIPINV
.= x by LTHIPP1 ;
hence (DES-PIPINV * DES-PIP) . x = x ; :: thesis: verum

end;

hence DES-PIPINV * DES-PIP = id (64 -tuples_on BOOLEAN) by L1, FUNCT_1:17; :: thesis: verum