reconsider f = ([#] Q1) --> (1. Q2) as Function of Q1,Q2 ;
take f ; :: thesis: f is homomorphic
thus f is homomorphic ; :: thesis: verum