set f = B2DB I;

thus B2DB I is onto by defB2DB; :: thesis: B2DB I is one-to-one

for x1, x2 being object st x1 in dom (B2DB I) & x2 in dom (B2DB I) & (B2DB I) . x1 = (B2DB I) . x2 holds

x1 = x2

thus B2DB I is onto by defB2DB; :: thesis: B2DB I is one-to-one

for x1, x2 being object st x1 in dom (B2DB I) & x2 in dom (B2DB I) & (B2DB I) . x1 = (B2DB I) . x2 holds

x1 = x2

proof

hence
B2DB I is one-to-one
; :: thesis: verum
let x1, x2 be object ; :: thesis: ( x1 in dom (B2DB I) & x2 in dom (B2DB I) & (B2DB I) . x1 = (B2DB I) . x2 implies x1 = x2 )

assume B1: ( x1 in dom (B2DB I) & x2 in dom (B2DB I) & (B2DB I) . x1 = (B2DB I) . x2 ) ; :: thesis: x1 = x2

B2: x1 in I by B1;

B5: x2 in I by B1;

B6: (ScProductDM L) . (x1,((B2DB I) . x2)) = 1 by B1, B2, defB2DB;

assume x1 <> x2 ; :: thesis: contradiction

hence contradiction by B2, B5, B6, defB2DB; :: thesis: verum

end;assume B1: ( x1 in dom (B2DB I) & x2 in dom (B2DB I) & (B2DB I) . x1 = (B2DB I) . x2 ) ; :: thesis: x1 = x2

B2: x1 in I by B1;

B5: x2 in I by B1;

B6: (ScProductDM L) . (x1,((B2DB I) . x2)) = 1 by B1, B2, defB2DB;

assume x1 <> x2 ; :: thesis: contradiction

hence contradiction by B2, B5, B6, defB2DB; :: thesis: verum