let X be non empty set ; :: thesis: for l being Linear_Combination of bspace X
for x being Element of (bspace X) st x in Carrier l holds
l . x = 1_ Z_2
let l be Linear_Combination of bspace X; :: thesis: for x being Element of (bspace X) st x in Carrier l holds
l . x = 1_ Z_2
let x be Element of (bspace X); :: thesis: ( x in Carrier l implies l . x = 1_ Z_2 )
assume A1: x in Carrier l ; :: thesis: l . x = 1_ Z_2
l . x <> 0. Z_2 by A1, VECTSP_6:20;
hence l . x = 1_ Z_2 by Th5, Th6, CARD_1:88, TARSKI:def 2; :: thesis: verum