let X be functional set ; :: thesis: ( ( for f, g being Function st f in X & g in X holds

f tolerates g ) implies union X is Function )

assume A1: for f, g being Function st f in X & g in X holds

f tolerates g ; :: thesis: union X is Function

A2: union X is Function-like

f tolerates g ) implies union X is Function )

assume A1: for f, g being Function st f in X & g in X holds

f tolerates g ; :: thesis: union X is Function

A2: union X is Function-like

proof

union X is Relation-like
let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in union X or not [x,y2] in union X or y1 = y2 )

assume that

A3: [x,y1] in union X and

A4: [x,y2] in union X and

A5: y1 <> y2 ; :: thesis: contradiction

consider gx being set such that

A6: [x,y2] in gx and

A7: gx in X by A4, TARSKI:def 4;

consider fx being set such that

A8: [x,y1] in fx and

A9: fx in X by A3, TARSKI:def 4;

reconsider fx = fx, gx = gx as Function by A9, A7;

fx tolerates gx by A1, A9, A7;

then ex h being Function st

( fx c= h & gx c= h ) by PARTFUN1:52;

hence contradiction by A5, A8, A6, FUNCT_1:def 1; :: thesis: verum

end;assume that

A3: [x,y1] in union X and

A4: [x,y2] in union X and

A5: y1 <> y2 ; :: thesis: contradiction

consider gx being set such that

A6: [x,y2] in gx and

A7: gx in X by A4, TARSKI:def 4;

consider fx being set such that

A8: [x,y1] in fx and

A9: fx in X by A3, TARSKI:def 4;

reconsider fx = fx, gx = gx as Function by A9, A7;

fx tolerates gx by A1, A9, A7;

then ex h being Function st

( fx c= h & gx c= h ) by PARTFUN1:52;

hence contradiction by A5, A8, A6, FUNCT_1:def 1; :: thesis: verum

proof

hence
union X is Function
by A2; :: thesis: verum
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in union X or ex b_{1}, b_{2} being object st x = [b_{1},b_{2}] )

assume x in union X ; :: thesis: ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]

then ex ux being set st

( x in ux & ux in X ) by TARSKI:def 4;

hence ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]
by RELAT_1:def 1; :: thesis: verum

end;assume x in union X ; :: thesis: ex b

then ex ux being set st

( x in ux & ux in X ) by TARSKI:def 4;

hence ex b