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

proof

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

end;

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