let X, X9 be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9
for a being Element of X st a is minimal holds
f . a is minimal
let f be BCI-homomorphism of X,X9; :: thesis: for a being Element of X st a is minimal holds
f . a is minimal
let a be Element of X; :: thesis: ( a is minimal implies f . a is minimal )
assume a is minimal ; :: thesis: f . a is minimal
then f . a = f . ((a `) `) by BCIALG_2:29;
then f . a = (f . (0. X)) \ (f . ((0. X) \ a)) by Def6;
then f . a = (f . (0. X)) \ ((f . (0. X)) \ (f . a)) by Def6;
then f . a = ((f . (0. X)) \ (f . a)) ` by Th35;
then f . a = ((f . a) `) ` by Th35;
hence f . a is minimal by BCIALG_2:29; :: thesis: verum