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
A3: ( a in x & x in X ) by TARSKI:def 4;
reconsider x = x as Function by A1, A3;
x = x ;
hence ex b, c being set st [b,c] = a by A3, 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 A4: ( [a,b] in union X & [a,c] in union X ) ; :: thesis: b = c
then consider x being set such that
A5: ( [a,b] in x & x in X ) by TARSKI:def 4;
consider y being set such that
A6: ( [a,c] in y & y in X ) by A4, TARSKI:def 4;
reconsider x = x as Function by A1, A5;
reconsider y = y as Function by A1, A6;
x,y are_c=-comparable by A2, A5, A6, ORDINAL1:def 9;
then ( x c= y or y c= x ) by XBOOLE_0:def 9;
hence b = c by A5, A6, FUNCT_1:def 1; :: thesis: verum