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 set st a in union X holds
ex b, c being set st [b,c] = a :: according to RELAT_1:def 1 :: thesis: union X is Function-like

proof

let a be set ; :: thesis: ( a in union X implies ex b, c being set st [b,c] = a )
assume a in union X ; :: thesis: ex b, c being set st [b,c] = a
then consider x being set such that
A4: a in x and
A5: x in X by TARSKI:def 4;
reconsider x = x as Function by A1, A5;
x = x ;
hence ex b, c being set st [b,c] = a by A4, RELAT_1:def 1; :: thesis: verum

end;

let a be set ; :: according to FUNCT_1:def 1 :: thesis: for b₁, b₂ being set holds
( not [a,b₁] in union X or not [a,b₂] in union X or b₁ = b₂ )
let b, c be set ; :: thesis: ( not [a,b] in union X or not [a,c] in union X or b = c )
assume that
A7: [a,b] in union X and
A8: [a,c] in union X ; :: thesis: b = c
consider x being set such that
A9: [a,b] in x and
A10: x in X by A7, TARSKI:def 4;
consider y being set such that
A11: [a,c] in y and
A12: y in X by A8, TARSKI:def 4;
reconsider x = x as Function by A1, A10;
reconsider y = y as Function by A1, A12;
x,y are_c=-comparable by A2, A10, A12, ORDINAL1:def 9;
then ( x c= y or y c= x ) by XBOOLE_0:def 9;
hence b = c by A9, A11, FUNCT_1:def 1; :: thesis: verum