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

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

hence
L1 = L2
; :: thesis: verumlet 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;thus L1 . h = LG . (h - g) by A6

.= L2 . h by A7 ; :: thesis: verum