theorem :: CAYLDICK:29

for N being non degenerated right_complementable almost_right_cancelable almost_left_invertible Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like well-unital distributive associative Banach_Algebra-like_2 Banach_Algebra-like_3 well-conjugated add-conjugative ConjNormAlgStr
for a, b being Element of N st ( not a is zero or not b is zero ) & <%a,b%> is right_mult-cancelable & <%a,b%> is left_invertible holds
/ <%a,b%> = <%((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')),((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b))%>