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
proof
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;
hence B2DB I is one-to-one ; :: thesis: verum