let n be Ordinal; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for x being Function of n,L holds eval (a | n,L),x = a
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for a being Element of L
for x being Function of n,L holds eval (a | n,L),x = a
let a be Element of L; :: thesis: for x being Function of n,L holds eval (a | n,L),x = a
let x be Function of n,L; :: thesis: eval (a | n,L),x = a
thus eval (a | n,L),x = coefficient (a | n,L) by Th24
.= a by Th23 ; :: thesis: verum