let X be LinearTopSpace; :: thesis: for A being Subset of X st X is T_1 holds
0 * (Cl A) = Cl (0 * A)
let A be Subset of X; :: thesis: ( X is T_1 implies 0 * (Cl A) = Cl (0 * A) )
assume A1: X is T_1 ; :: thesis: 0 * (Cl A) = Cl (0 * A)
per cases ( A is empty or not A is empty ) ;
suppose A2: A is empty ; :: thesis: 0 * (Cl A) = Cl (0 * A)
then A3: Cl A = {} X by PRE_TOPC:22;
hence 0 * (Cl A) = {} X by CONVEX1:33
.= Cl (0 * A) by A2, A3, CONVEX1:33 ;
:: thesis: verum
end;
suppose A4: not A is empty ; :: thesis: 0 * (Cl A) = Cl (0 * A)
then not Cl A is empty by PRE_TOPC:18, XBOOLE_1:3;
hence 0 * (Cl A) = {(0. X)} by CONVEX1:34
.= Cl {(0. X)} by A1, YELLOW_8:26
.= Cl (0 * A) by A4, CONVEX1:34 ;
:: thesis: verum
end;
end;