let X, X9 be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9
for a being Element of AtomSet X
for b being Element of AtomSet X9 st b = f . a holds
f .: (BranchV a) c= BranchV b
let f be BCI-homomorphism of X,X9; :: thesis: for a being Element of AtomSet X
for b being Element of AtomSet X9 st b = f . a holds
f .: (BranchV a) c= BranchV b
let a be Element of AtomSet X; :: thesis: for b being Element of AtomSet X9 st b = f . a holds
f .: (BranchV a) c= BranchV b
let b be Element of AtomSet X9; :: thesis: ( b = f . a implies f .: (BranchV a) c= BranchV b )
assume A1: b = f . a ; :: thesis: f .: (BranchV a) c= BranchV b
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (BranchV a) or y in BranchV b )
assume y in f .: (BranchV a) ; :: thesis: y in BranchV b
then consider x being object such that
x in dom f and
A2: x in BranchV a and
A3: y = f . x by FUNCT_1:def 6;
A4: ex x1 being Element of X st
( x = x1 & a <= x1 ) by A2;
reconsider x = x as Element of X by A2;
(f . a) \ (f . x) = f . (a \ x) by Def6;
then (f . a) \ (f . x) = f . (0. X) by A4;
then (f . a) \ (f . x) = 0. X9 by Th35;
then b <= f . x by A1;
hence y in BranchV b by A3; :: thesis: verum