let C1, C2 be Subset of (DivisibleMod L); :: thesis: ( ( for v being Vector of (DivisibleMod L) holds

( v in C1 iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) ) & ( for v being Vector of (DivisibleMod L) holds

( v in C2 iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) ) implies C1 = C2 )

assume that

A1: for v being Vector of (DivisibleMod L) holds

( v in C1 iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) and

A2: for v being Vector of (DivisibleMod L) holds

( v in C2 iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) ; :: thesis: C1 = C2

for v being Vector of (DivisibleMod L) st v in C1 holds

v in C2

for v being Vector of (DivisibleMod L) st v in C2 holds

v in C1

hence C1 = C2 by A3; :: thesis: verum

( v in C1 iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) ) & ( for v being Vector of (DivisibleMod L) holds

( v in C2 iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) ) implies C1 = C2 )

assume that

A1: for v being Vector of (DivisibleMod L) holds

( v in C1 iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) and

A2: for v being Vector of (DivisibleMod L) holds

( v in C2 iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) ; :: thesis: C1 = C2

for v being Vector of (DivisibleMod L) st v in C1 holds

v in C2

proof

then A3:
C1 c= C2
;
let v be Vector of (DivisibleMod L); :: thesis: ( v in C1 implies v in C2 )

assume B1: v in C1 ; :: thesis: v in C2

ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) by A1, B1;

hence v in C2 by A2; :: thesis: verum

end;assume B1: v in C1 ; :: thesis: v in C2

ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) by A1, B1;

hence v in C2 by A2; :: thesis: verum

for v being Vector of (DivisibleMod L) st v in C2 holds

v in C1

proof

then
C2 c= C1
;
let v be Vector of (DivisibleMod L); :: thesis: ( v in C2 implies v in C1 )

assume B1: v in C2 ; :: thesis: v in C1

ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) by A2, B1;

hence v in C1 by A1; :: thesis: verum

end;assume B1: v in C2 ; :: thesis: v in C1

ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) by A2, B1;

hence v in C1 by A1; :: thesis: verum

hence C1 = C2 by A3; :: thesis: verum