per cases ( L is trivial or not L is trivial ) ;

suppose L is trivial ; :: thesis: ex b₁ being Function of I,(DualBasis I) st
( dom b₁ = I & rng b₁ = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(b₁ . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(b₁ . v)) = 0 ) ) ) )

then (Omega). L = (0). L by ZMODUL07:41;
then rank L = 0 by ZMODUL05:1;
then rank (EMLat L) = 0 by ZMODLAT2:42;
then A1: card I = 0 by ZMODUL03:def 5;
for v being Vector of (DivisibleMod L) holds
( v in {} 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 ) ) ) by A1;
then A2: DualBasis I = {} the carrier of (DivisibleMod L) by defDualBasis;
set F = the Function of I,(DualBasis I);
take the Function of I,(DualBasis I) ; :: thesis: ( dom the Function of I,(DualBasis I) = I & rng the Function of I,(DualBasis I) = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,( the Function of I,(DualBasis I) . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,( the Function of I,(DualBasis I) . v)) = 0 ) ) ) )
I = {} by A1;
hence ( dom the Function of I,(DualBasis I) = I & rng the Function of I,(DualBasis I) = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,( the Function of I,(DualBasis I) . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,( the Function of I,(DualBasis I) . v)) = 0 ) ) ) ) by A2; :: thesis: verum

end;

suppose X1: not L is trivial ; :: thesis: ex b₁ being Function of I,(DualBasis I) st
( dom b₁ = I & rng b₁ = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(b₁ . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(b₁ . v)) = 0 ) ) ) )

defpred S₁[ object , object ] means ( (ScProductDM L) . ($1,$2) = 1 & ( for w being Vector of (EMLat L) st w in I & $1 <> w holds
(ScProductDM L) . (w,$2) = 0 ) );
consider b being FinSequence such that
A0: ( rng b = I & b is one-to-one ) by FINSEQ_4:58;
b is FinSequence of (EMLat L) by A0, FINSEQ_1:def 4;
then reconsider b = b as OrdBasis of EMLat L by A0, ZMATRLIN:def 5;
A1: for x being object st x in I holds
ex y being object st
( y in DualBasis I & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in I implies ex y being object st
( y in DualBasis I & S₁[x,y] ) )
assume B1: x in I ; :: thesis: ex y being object st
( y in DualBasis I & S₁[x,y] )
consider i being Nat such that
B3: ( i in dom b & b . i = x ) by A0, B1, FINSEQ_2:10;
b /. i = x by B3, PARTFUN1:def 6;
then consider y being Vector of (DivisibleMod L) such that
B4: ( (ScProductDM L) . (x,y) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),y) = 0 ) ) by X1, B3, LmDE31;
B5: for w being Vector of (EMLat L) st w in I & x <> w holds
(ScProductDM L) . (w,y) = 0

proof

let w be Vector of (EMLat L); :: thesis: ( w in I & x <> w implies (ScProductDM L) . (w,y) = 0 )
assume C1: ( w in I & x <> w ) ; :: thesis: (ScProductDM L) . (w,y) = 0
consider j being Nat such that
C2: ( j in dom b & b . j = w ) by A0, C1, FINSEQ_2:10;
b /. j = w by C2, PARTFUN1:def 6;
hence (ScProductDM L) . (w,y) = 0 by B3, B4, C1, C2; :: thesis: verum

end;

take y ; :: thesis: ( y in DualBasis I & S₁[x,y] )
thus ( y in DualBasis I & S₁[x,y] ) by B1, B4, B5, defDualBasis; :: thesis: verum

end;

consider f being Function such that
A2: ( dom f = I & rng f c= DualBasis I & ( for x being object st x in I holds
S₁[x,f . x] ) ) from FUNCT_1:sch 6(A1);
A3: DualBasis I c= rng f

proof

for y being object st y in DualBasis I holds
ex x being object st
( x in dom f & y = f . x )

proof

let y be object ; :: thesis: ( y in DualBasis I implies ex x being object st
( x in dom f & y = f . x ) )
assume B1: y in DualBasis I ; :: thesis: ex x being object st
( x in dom f & y = f . x )
consider u being Vector of (EMLat L) such that
B2: ( u in I & (ScProductDM L) . (u,y) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,y) = 0 ) ) by B1, defDualBasis;
take u ; :: thesis: ( u in dom f & y = f . u )
consider i being Nat such that
B6: ( i in dom b & b . i = u ) by A0, B2, FINSEQ_2:10;
B8: for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),y) = (ScProductDM L) . ((b /. n),(f . u))

proof

let n be Nat; :: thesis: ( n in dom b implies (ScProductDM L) . ((b /. n),y) = (ScProductDM L) . ((b /. n),(f . u)) )
assume C1: n in dom b ; :: thesis: (ScProductDM L) . ((b /. n),y) = (ScProductDM L) . ((b /. n),(f . u))

per cases ( n = i or n <> i ) ;

suppose C2: n = i ; :: thesis: (ScProductDM L) . ((b /. n),y) = (ScProductDM L) . ((b /. n),(f . u))

hence (ScProductDM L) . ((b /. n),y) = (ScProductDM L) . (u,y) by B6, PARTFUN1:def 6
.= (ScProductDM L) . (u,(f . u)) by A2, B2
.= (ScProductDM L) . ((b /. n),(f . u)) by B6, C2, PARTFUN1:def 6 ;
:: thesis: verum

end;

suppose n <> i ; :: thesis: (ScProductDM L) . ((b /. n),y) = (ScProductDM L) . ((b /. n),(f . u))

then b . n <> b . i by A0, B6, C1;
then C2: b /. n <> u by B6, C1, PARTFUN1:def 6;
b . n in rng b by C1, FUNCT_1:3;
then C3: b /. n in I by A0, C1, PARTFUN1:def 6;
hence (ScProductDM L) . ((b /. n),y) = 0 by B2, C2
.= (ScProductDM L) . ((b /. n),(f . u)) by A2, B2, C2, C3 ;
:: thesis: verum

end;

end;

end;

f . u in DualBasis I by A2, B2, FUNCT_1:3;
hence ( u in dom f & y = f . u ) by A2, B1, B2, B8, ZMODLAT2:63; :: thesis: verum

end;

hence DualBasis I c= rng f by FUNCT_1:9; :: thesis: verum

end;

then rng f = DualBasis I by A2;
then reconsider f = f as Function of I,(DualBasis I) by A2, FUNCT_2:1;
take f ; :: thesis: ( dom f = I & rng f = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(f . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(f . v)) = 0 ) ) ) )
thus ( dom f = I & rng f = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(f . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(f . v)) = 0 ) ) ) ) by A2, A3; :: thesis: verum

end;

end;