let s be non empty typealg ; :: thesis: for p being Proof of s
for v being Element of dom p holds
( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 )
let p be Proof of s; :: thesis: for v being Element of dom p holds
( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 )
let v be Element of dom p; :: thesis: ( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 )
v is correct by Def13;
hence ( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 ) by Def5; :: thesis: verum