let f be Function; :: thesis: for A being set st A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) holds
union A in sproduct f
let A be set ; :: thesis: ( A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) implies union A in sproduct f )
assume that
A1: A c= sproduct f and
A2: for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ; :: thesis: union A in sproduct f
reconsider g = union A as Function by A1, A2, PARTFUN1:188;
A3: dom g c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in dom f )
assume x in dom g ; :: thesis: x in dom f
then consider y being set such that
A4: [x,y] in g by RELAT_1:def 4;
consider h being set such that
A5: [x,y] in h and
A6: h in A by A4, TARSKI:def 4;
reconsider h = h as Function by A1, A6;
A7: x in dom h by A5, RELAT_1:def 4;
dom h c= dom f by A1, A6, Th65;
hence x in dom f by A7; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom g implies g . x in f . x )
assume x in dom g ; :: thesis: g . x in f . x
then consider y being set such that
A8: [x,y] in g by RELAT_1:def 4;
consider h being set such that
A9: [x,y] in h and
A10: h in A by A8, TARSKI:def 4;
reconsider h = h as Function by A1, A10;
A11: x in dom h by A9, RELAT_1:def 4;
h . x = y by A9, FUNCT_1:8
.= g . x by A8, FUNCT_1:8 ;
hence g . x in f . x by A1, A10, A11, Th65; :: thesis: verum

end;

hence union A in sproduct f by A3, Def9; :: thesis: verum