let L1, L2 be Linear_Combination of G; :: thesis: ( ( for h being Element of G holds L1 . h = LG . (h - g) ) & ( for h being Element of G holds L2 . h = LG . (h - g) ) implies L1 = L2 )
assume that
A6: for h being Element of G holds L1 . h = LG . (h - g) and
A7: for h being Element of G holds L2 . h = LG . (h - g) ; :: thesis: L1 = L2

now :: thesis: for h being Element of G holds L1 . h = L2 . h

let h be Element of G; :: thesis: L1 . h = L2 . h
thus L1 . h = LG . (h - g) by A6
.= L2 . h by A7 ; :: thesis: verum

end;

hence L1 = L2 ; :: thesis: verum