let X be set ; :: thesis: ( ( X is functional & X is compatible ) iff union X is Function )
now
assume A1: union X is Function ; :: thesis: ( X is functional & X is compatible )
thus X is functional :: thesis: X is compatible
proof
let f be set ; :: according to FUNCT_1:def 19 :: thesis: ( not f in X or f is set )
assume A2: f in X ; :: thesis: f is set
A3: f is Function-like
proof
let x, y1, y2 be set ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in f or not [x,y2] in f or y1 = y2 )
assume that
A4: [x,y1] in f and
A5: [x,y2] in f ; :: thesis: y1 = y2
A6: [x,y2] in union X by A2, A5, TARSKI:def 4;
[x,y1] in union X by A2, A4, TARSKI:def 4;
hence y1 = y2 by A1, A6, FUNCT_1:def 1; :: thesis: verum
end;
f is Relation-like
proof
let x be set ; :: according to RELAT_1:def 1 :: thesis: ( not x in f or ex b1, b2 being set st x = [b1,b2] )
assume x in f ; :: thesis: ex b1, b2 being set st x = [b1,b2]
then x in union X by A2, TARSKI:def 4;
hence ex b1, b2 being set st x = [b1,b2] by A1, RELAT_1:def 1; :: thesis: verum
end;
hence f is set by A3; :: thesis: verum
end;
thus X is compatible :: thesis: verum
proof
let f, g be Function; :: according to COMPUT_1:def 1 :: thesis: ( f in X & g in X implies f tolerates g )
assume that
A7: f in X and
A8: g in X ; :: thesis: f tolerates g
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (proj1 f) /\ (proj1 g) or f . x = g . x )
assume A9: x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then A10: x in dom g by XBOOLE_0:def 4;
then consider y2 being set such that
A11: [x,y2] in g by RELAT_1:def 4;
A12: [x,y2] in union X by A8, A11, TARSKI:def 4;
A13: x in dom f by A9, XBOOLE_0:def 4;
then consider y1 being set such that
A14: [x,y1] in f by RELAT_1:def 4;
[x,y1] in union X by A7, A14, TARSKI:def 4;
then A15: y1 = y2 by A1, A12, FUNCT_1:def 1;
thus f . x = y1 by A13, A14, FUNCT_1:def 4
.= g . x by A10, A11, A15, FUNCT_1:def 4 ; :: thesis: verum
end;
end;
hence ( ( X is functional & X is compatible ) iff union X is Function ) ; :: thesis: verum