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

end;

suppose
L is trivial
; :: thesis: ex b_{1} being Function of I,(DualBasis I) st

( dom b_{1} = I & rng b_{1} = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(b_{1} . v)) = 0 ) ) ) )

( dom b

( (ScProductDM L) . (v,(b

(ScProductDM L) . (w,(b

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;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

suppose X1:
not L is trivial
; :: thesis: ex b_{1} being Function of I,(DualBasis I) st

( dom b_{1} = I & rng b_{1} = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(b_{1} . v)) = 0 ) ) ) )

( dom b

( (ScProductDM L) . (v,(b

(ScProductDM L) . (w,(b

defpred S_{1}[ 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_{1}[x,y] )

A2: ( dom f = I & rng f c= DualBasis I & ( for x being object st x in I holds

S_{1}[x,f . x] ) )
from FUNCT_1:sch 6(A1);

A3: DualBasis I c= rng f

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;(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

proof

consider f being Function such that
let x be object ; :: thesis: ( x in I implies ex y being object st

( y in DualBasis I & S_{1}[x,y] ) )

assume B1: x in I ; :: thesis: ex y being object st

( y in DualBasis I & S_{1}[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_{1}[x,y] )

thus ( y in DualBasis I & S_{1}[x,y] )
by B1, B4, B5, defDualBasis; :: thesis: verum

end;( y in DualBasis I & S

assume B1: x in I ; :: thesis: ex y being object st

( y in DualBasis I & S

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

take
y
; :: thesis: ( y in DualBasis I & S
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;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

thus ( y in DualBasis I & S

A2: ( dom f = I & rng f c= DualBasis I & ( for x being object st x in I holds

S

A3: DualBasis I c= rng f

proof

then
rng f = DualBasis I
by A2;
for y being object st y in DualBasis I holds

ex x being object st

( x in dom f & y = f . x )

end;ex x being object st

( x in dom f & y = f . x )

proof

hence
DualBasis I c= rng f
by FUNCT_1:9; :: thesis: verum
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))

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

end;( 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

f . u in DualBasis I
by A2, B2, FUNCT_1:3;
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))

end;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 )
;

end;

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;.= (ScProductDM L) . (u,(f . u)) by A2, B2

.= (ScProductDM L) . ((b /. n),(f . u)) by B6, C2, PARTFUN1:def 6 ;

:: thesis: verum

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;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

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

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