let f, g, h be Function; :: thesis: ( g tolerates h & g in sproduct f & h in sproduct f implies g \/ h in sproduct f )
assume that
A1: g tolerates h and
A2: g in sproduct f and
A3: h in sproduct f ; :: thesis: g \/ h in sproduct f
A4: {g,h} c= sproduct f by A2, A3, ZFMISC_1:32;
A5: now :: thesis: for h1, h2 being Function st h1 in {g,h} & h2 in {g,h} holds
h1 tolerates h2
let h1, h2 be Function; :: thesis: ( h1 in {g,h} & h2 in {g,h} implies h1 tolerates h2 )
assume that
A6: h1 in {g,h} and
A7: h2 in {g,h} ; :: thesis: h1 tolerates h2
A8: ( h1 = g or h1 = h ) by A6, TARSKI:def 2;
( h2 = g or h2 = h ) by A7, TARSKI:def 2;
hence h1 tolerates h2 by A1, A8; :: thesis: verum
end;
union {g,h} = g \/ h by ZFMISC_1:75;
hence g \/ h in sproduct f by A4, A5, Th62; :: thesis: verum