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