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