let MCFunc be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))); :: thesis: for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (MCFunc ") . (MCFunc . input) = input
let input be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: (MCFunc ") . (MCFunc . input) = input
thus (MCFunc ") . (MCFunc . input) = ((MCFunc ") * MCFunc) . input by FUNCT_2:15
.= (id (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))) . input by FUNCT_2:61
.= input ; :: thesis: verum