let X be set ; :: thesis: ( ( for x being set st x in X holds
x is Function ) & X is c=-linear implies ( union X is Relation-like & union X is Function-like ) )
assume that
A1: for x being set st x in X holds
x is Function and
A2: X is c=-linear ; :: thesis: ( union X is Relation-like & union X is Function-like )
thus for a being object st a in union X holds
ex b, c being object st [b,c] = a :: according to RELAT_1:def 1 :: thesis: union X is Function-like
proof
let a be object ; :: thesis: ( a in union X implies ex b, c being object st [b,c] = a )
assume a in union X ; :: thesis: ex b, c being object st [b,c] = a
then consider x being set such that
A3: a in x and
A4: x in X by TARSKI:def 4;
reconsider x = x as Function by A1, A4;
x = x ;
hence ex b, c being object st [b,c] = a by A3, RELAT_1:def 1; :: thesis: verum
end;
let a, b, c be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [a,b] in union X or not [a,c] in union X or b = c )
assume that
A5: [a,b] in union X and
A6: [a,c] in union X ; :: thesis: b = c
consider x being set such that
A7: [a,b] in x and
A8: x in X by A5, TARSKI:def 4;
consider y being set such that
A9: [a,c] in y and
A10: y in X by A6, TARSKI:def 4;
reconsider x = x as Function by A1, A8;
reconsider y = y as Function by A1, A10;
x,y are_c=-comparable by A2, A8, A10;
then ( x c= y or y c= x ) ;
hence b = c by A7, A9, FUNCT_1:def 1; :: thesis: verum