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

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