reconsider f = the carrier of X --> (0. X9) as Function of X,X9 ;
take f ; :: thesis: f is multiplicative
for x, y being Element of X holds f . (x \ y) = (f . x) \ (f . y)

proof

let x, y be Element of X; :: thesis: f . (x \ y) = (f . x) \ (f . y)
f . (x \ y) = 0. X9 by FUNCOP_1:7
.= (0. X9) ` by BCIALG_1:2
.= (f . x) \ (0. X9) by FUNCOP_1:7 ;
hence f . (x \ y) = (f . x) \ (f . y) by FUNCOP_1:7; :: thesis: verum

end;

hence f is multiplicative ; :: thesis: verum