let A be set ; :: thesis: for K being Element of Normal_forms_on A holds mi (K ^ K) = K
let K be Element of Normal_forms_on A; :: thesis: mi (K ^ K) = K
thus mi (K ^ K) = mi K by NORMFORM:55
.= K by NORMFORM:42 ; :: thesis: verum