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

proof

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

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

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

hence f1 . x = f2 . x ; :: thesis: verum

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

proof

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;

per cases ( b /. n = x or b /. n <> x ) ;

suppose B3: b /. n = x ; :: thesis: (ScProductDM L) . ((b /. n),(f1 . x)) = (ScProductDM L) . ((b /. n),(f2 . x))

hence (ScProductDM L) . ((b /. n),(f1 . x)) = 1 by AS1, B2
.= (ScProductDM L) . ((b /. n),(f2 . x)) by AS2, B2, B3 ;
:: thesis: verum

end;

suppose B4: b /. n <> x ; :: thesis: (ScProductDM L) . ((b /. n),(f1 . x)) = (ScProductDM L) . ((b /. n),(f2 . x))

hence (ScProductDM L) . ((b /. n),(f1 . x)) = 0 by AS1, X1, B2X
.= (ScProductDM L) . ((b /. n),(f2 . x)) by AS2, X1, B2X, B4 ;
:: thesis: verum

end;

end;

end;

A2: f1 . x in DualBasis I by AS1, XX1, FUNCT_1:3;
f2 . x in DualBasis I by AS2, XX1, FUNCT_1:3;
hence f1 . x = f2 . x by A1, A2, ZMODLAT2:63; :: thesis: verum

end;

end;

end;

hence f1 = f2 ; :: thesis: verum