let x be Element of ExtREAL ; :: thesis: x |^ 1 = x
Product (1 |-> x) = Product <*x*> by FINSEQ_2:59;
hence x |^ 1 = x by Th7; :: thesis: verum