set f = coprod (i,A);
thus coprod (i,A) is Relation-like :: thesis: coprod (i,A) is Function-like
proof
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in coprod (i,A) or ex b1, b2 being object st x = [b1,b2] )
assume x in coprod (i,A) ; :: thesis: ex b1, b2 being object st x = [b1,b2]
then ex a being set st
( a in A . i & x = [a,i] ) by MSAFREE:def 2;
hence ex b1, b2 being object st x = [b1,b2] ; :: thesis: verum
end;
let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in coprod (i,A) or not [x,y2] in coprod (i,A) or y1 = y2 )
assume [x,y1] in coprod (i,A) ; :: thesis: ( not [x,y2] in coprod (i,A) or y1 = y2 )
then A1: ex a being set st
( a in A . i & [x,y1] = [a,i] ) by MSAFREE:def 2;
assume [x,y2] in coprod (i,A) ; :: thesis: y1 = y2
then ex b being set st
( b in A . i & [x,y2] = [b,i] ) by MSAFREE:def 2;
then ( y1 = i & y2 = i ) by A1, XTUPLE_0:1;
hence y1 = y2 ; :: thesis: verum