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:78;
A3: dom g c= dom f
proof
let x be object ; :: 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 object such that
A4: [x,y] in g by XTUPLE_0:def 12;
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, XTUPLE_0:def 12;
dom h c= dom f by A1, A6, Th49;
hence x in dom f by A7; :: thesis: verum
end;
now :: thesis: for x being object st x in dom g holds
g . x in f . x
let x be object ; :: 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 object such that
A8: [x,y] in g by XTUPLE_0:def 12;
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, XTUPLE_0:def 12;
h . x = y by A9, FUNCT_1:1
.= g . x by A8, FUNCT_1:1 ;
hence g . x in f . x by A1, A10, A11, Th49; :: thesis: verum
end;
hence union A in sproduct f by A3, Def9; :: thesis: verum