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

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