let f, g be Function; :: thesis: fixpoints [:f,g:] = [:(fixpoints f),(fixpoints g):]
set h = [:f,g:];
set F = fixpoints f;
set G = fixpoints g;
set LH = fixpoints [:f,g:];
set RH = [:(fixpoints f),(fixpoints g):];
set df = dom f;
set dg = dom g;
[:f,g:] /\ (id (dom [:f,g:])) = [:f,g:] /\ (id [:(dom f),(dom g):]) by FUNCT_3:def 8
.= [:f,g:] /\ [:(id (dom f)),(id (dom g)):] by FUNCT_3:69
.= [:(f /\ (id (dom f))),(g /\ (id (dom g))):] by Lm76 ;
hence fixpoints [:f,g:] = [:(fixpoints f),(fixpoints g):] by FUNCT_3:def 8; :: thesis: verum