let L be positive-definite RATional Z_Lattice; :: thesis: for b being OrdBasis of EMLat L
for I being Basis of (EMLat L) st I = rng b holds
(B2DB I) * b is OrdBasis of DualLat L
let b be OrdBasis of EMLat L; :: thesis: for I being Basis of (EMLat L) st I = rng b holds
(B2DB I) * b is OrdBasis of DualLat L
let I be Basis of (EMLat L); :: thesis: ( I = rng b implies (B2DB I) * b is OrdBasis of DualLat L )
assume A1: I = rng b ; :: thesis: (B2DB I) * b is OrdBasis of DualLat L
A2: b is one-to-one by ZMATRLIN:def 5;
b is FinSequence of I by A1, FINSEQ_1:def 4;
then A3: (B2DB I) * b is FinSequence of DualBasis I by FINSEQ_2:32;
A4: dom (B2DB I) = I by defB2DB;
A5: rng ((B2DB I) * b) = (B2DB I) .: (rng b) by RELAT_1:127
.= rng (B2DB I) by A1, A4, RELAT_1:113
.= DualBasis I by defB2DB ;
DualBasis I is Subset of (DualLat L) by ThDLDB;
then A6: (B2DB I) * b is FinSequence of (DualLat L) by A3, A5, FINSEQ_1:def 4;
rng ((B2DB I) * b) is Basis of (DualLat L) by A5, ThDLDB;
hence (B2DB I) * b is OrdBasis of DualLat L by A2, A6, ZMATRLIN:def 5; :: thesis: verum