let f1, f2 be Function of I,(); :: thesis: ( dom f1 = I & rng f1 = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(f1 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(f1 . v)) = 0 ) ) ) & dom f2 = I & rng f2 = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(f2 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(f2 . v)) = 0 ) ) ) implies f1 = f2 )

assume AS1: ( dom f1 = I & rng f1 = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(f1 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(f1 . v)) = 0 ) ) ) ) ; :: thesis: ( not dom f2 = I or not rng f2 = DualBasis I or ex v being Vector of () st
( v in I & not ( () . (v,(f2 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(f2 . v)) = 0 ) ) ) or f1 = f2 )

assume AS2: ( dom f2 = I & rng f2 = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(f2 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (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 () by ;
then reconsider b = b as OrdBasis of EMLat L by ;
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
() . ((b /. n),(f1 . x)) = () . ((b /. n),(f2 . x))
proof
let n be Nat; :: thesis: ( n in dom b implies () . ((b /. n),(f1 . x)) = () . ((b /. n),(f2 . x)) )
assume B1: n in dom b ; :: thesis: () . ((b /. n),(f1 . x)) = () . ((b /. n),(f2 . x))
B2: b . n in I by ;
then B2X: b /. n in I by ;
per cases ( b /. n = x or b /. n <> x ) ;
suppose B3: b /. n = x ; :: thesis: () . ((b /. n),(f1 . x)) = () . ((b /. n),(f2 . x))
hence () . ((b /. n),(f1 . x)) = 1 by
.= () . ((b /. n),(f2 . x)) by AS2, B2, B3 ;
:: thesis: verum
end;
suppose B4: b /. n <> x ; :: thesis: () . ((b /. n),(f1 . x)) = () . ((b /. n),(f2 . x))
hence () . ((b /. n),(f1 . x)) = 0 by AS1, X1, B2X
.= () . ((b /. n),(f2 . x)) by AS2, X1, B2X, B4 ;
:: thesis: verum
end;
end;
end;
A2: f1 . x in DualBasis I by ;
f2 . x in DualBasis I by ;
hence f1 . x = f2 . x by ; :: thesis: verum
end;
end;
end;
hence f1 = f2 ; :: thesis: verum