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