let f1, f2 be Function of I,(DualBasis I); :: thesis: ( dom f1 = I & rng f1 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(f1 . v)) = 0 ) ) ) & dom f2 = I & rng f2 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(f2 . v)) = 0 ) ) ) implies f1 = f2 )

assume AS1: ( dom f1 = I & rng f1 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(f1 . v)) = 0 ) ) ) ) ; :: thesis: ( not dom f2 = I or not rng f2 = DualBasis I or ex v being Vector of (EMLat L) st

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

(ScProductDM L) . (w,(f2 . v)) = 0 ) ) ) or f1 = f2 )

assume AS2: ( dom f2 = I & rng f2 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(f2 . v)) = 0 ) ) ) ) ; :: thesis: f1 = f2

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;

for x being Element of I holds f1 . x = f2 . x

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

(ScProductDM L) . (w,(f1 . v)) = 0 ) ) ) & dom f2 = I & rng f2 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(f2 . v)) = 0 ) ) ) implies f1 = f2 )

assume AS1: ( dom f1 = I & rng f1 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(f1 . v)) = 0 ) ) ) ) ; :: thesis: ( not dom f2 = I or not rng f2 = DualBasis I or ex v being Vector of (EMLat L) st

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

(ScProductDM L) . (w,(f2 . v)) = 0 ) ) ) or f1 = f2 )

assume AS2: ( dom f2 = I & rng f2 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

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

(ScProductDM L) . (w,(f2 . v)) = 0 ) ) ) ) ; :: thesis: f1 = f2

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;

for x being Element of I holds f1 . x = f2 . x

proof

hence
f1 = f2
; :: thesis: verum
let x be Element of I; :: thesis: f1 . x = f2 . x

end;per cases
( I is empty or not I is empty )
;

end;

suppose XX1:
not I is empty
; :: thesis: f1 . x = f2 . x

then X1:
x in I
;

A1: for n being Nat st n in dom b holds

(ScProductDM L) . ((b /. n),(f1 . x)) = (ScProductDM L) . ((b /. n),(f2 . x))

f2 . x in DualBasis I by AS2, XX1, FUNCT_1:3;

hence f1 . x = f2 . x by A1, A2, ZMODLAT2:63; :: thesis: verum

end;A1: for n being Nat st n in dom b holds

(ScProductDM L) . ((b /. n),(f1 . x)) = (ScProductDM L) . ((b /. n),(f2 . x))

proof

A2:
f1 . x in DualBasis I
by AS1, XX1, FUNCT_1:3;
let n be Nat; :: thesis: ( n in dom b implies (ScProductDM L) . ((b /. n),(f1 . x)) = (ScProductDM L) . ((b /. n),(f2 . x)) )

assume B1: n in dom b ; :: thesis: (ScProductDM L) . ((b /. n),(f1 . x)) = (ScProductDM L) . ((b /. n),(f2 . x))

B2: b . n in I by A0, B1, FUNCT_1:3;

then B2X: b /. n in I by B1, PARTFUN1:def 6;

end;assume B1: n in dom b ; :: thesis: (ScProductDM L) . ((b /. n),(f1 . x)) = (ScProductDM L) . ((b /. n),(f2 . x))

B2: b . n in I by A0, B1, FUNCT_1:3;

then B2X: b /. n in I by B1, PARTFUN1:def 6;

f2 . x in DualBasis I by AS2, XX1, FUNCT_1:3;

hence f1 . x = f2 . x by A1, A2, ZMODLAT2:63; :: thesis: verum