theorem :: FOMODEL0:76

for f, g being Function holds fixpoints [:f,g:] = [:(fixpoints f),(fixpoints g):] by Lm79;