let f be Function of Q1,Q2; :: thesis: ( f = ([#] Q1) --> (1. Q2) implies f is homomorphic )
assume A1: f = ([#] Q1) --> (1. Q2) ; :: thesis: f is homomorphic
thus f . (1. Q1) = 1. Q2 by A1; :: according to AIMLOOP:def 28,AIMLOOP:def 30 :: thesis: f is quasi-homomorphic
thus f is quasi-homomorphic by A1; :: thesis: verum