let X be set ; ( ( 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
; ( 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
RELAT_1:def 1 union X is Function-like
let a, b, c be object ; FUNCT_1:def 1 ( 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
; 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; verum