let X, Y be set ; :: thesis: for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)
let f be Function; :: thesis: (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)
set Z = X \/ Y;
( f | X c= f & f | Y c= f ) by RELAT_1:88;
then f | X tolerates f | Y by PARTFUN1:131;
then A1: (f | X) \/ (f | Y) = (f | X) +* (f | Y) by FUNCT_4:31;
A2: ( dom (f | X) = (dom f) /\ X & dom (f | Y) = (dom f) /\ Y ) by RELAT_1:90;
then ( dom (f | X) c= dom f & dom (id Y) c= Y ) by XBOOLE_1:17;
then A3: (dom (f | X)) /\ (dom (id Y)) c= dom (f | Y) by A2, XBOOLE_1:27;
thus (X \/ Y) -indexing f = ((id X) +* (id Y)) +* (f | (X \/ Y)) by FUNCT_4:23
.= ((id X) +* (id Y)) +* ((f | X) +* (f | Y)) by A1, RELAT_1:107
.= (id X) +* ((id Y) +* ((f | X) +* (f | Y))) by FUNCT_4:15
.= (id X) +* (((id Y) +* (f | X)) +* (f | Y)) by FUNCT_4:15
.= (id X) +* (((f | X) +* (id Y)) +* (f | Y)) by A3, Th1
.= (id X) +* ((f | X) +* ((id Y) +* (f | Y))) by FUNCT_4:15
.= (X -indexing f) +* (Y -indexing f) by FUNCT_4:15 ; :: thesis: verum