let X be set ; :: thesis: ( ( X is functional & X is compatible ) iff union X is Function )
now :: thesis: ( union X is Function implies ( X is functional & X is compatible ) )
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 object ; :: according to FUNCT_1:def 13 :: thesis: ( not f in X or f is set )
assume A2: f in X ; :: thesis: f is set
reconsider f = f as set by TARSKI:1;
A3: f is Function-like
proof
let x, y1, y2 be object ; :: 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 object ; :: according to RELAT_1:def 1 :: thesis: ( not x in f or ex b1, b2 being object st x = [b1,b2] )
assume x in f ; :: thesis: ex b1, b2 being object st x = [b1,b2]
then x in union X by A2, TARSKI:def 4;
hence ex b1, b2 being object 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 object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom f) /\ (dom 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 object such that
A11: [x,y2] in g by XTUPLE_0:def 12;
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 object such that
A14: [x,y1] in f by XTUPLE_0:def 12;
A15: y1 is set by TARSKI:1;
[x,y1] in union X by A7, A14, TARSKI:def 4;
then A16: y1 = y2 by A1, A12, FUNCT_1:def 1;
thus f . x = y1 by A13, A14, FUNCT_1:def 2, A15
.= g . x by A10, A11, A16, FUNCT_1:def 2, A15 ; :: thesis: verum
end;
end;
hence ( ( X is functional & X is compatible ) iff union X is Function ) ; :: thesis: verum