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;
A1: f | Y c= f by RELAT_1:59;
f | X c= f by RELAT_1:59;
then f | X tolerates f | Y by A1, PARTFUN1:52;
then A2: (f | X) \/ (f | Y) = (f | X) +* (f | Y) by FUNCT_4:30;
dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A3: dom (f | X) c= dom f by XBOOLE_1:17;
dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then A4: (dom (f | X)) /\ (dom (id Y)) c= dom (f | Y) by A3, XBOOLE_1:27;
thus (X \/ Y) -indexing f = ((id X) +* (id Y)) +* (f | (X \/ Y)) by FUNCT_4:22
.= ((id X) +* (id Y)) +* ((f | X) +* (f | Y)) by A2, RELAT_1:78
.= (id X) +* ((id Y) +* ((f | X) +* (f | Y))) by FUNCT_4:14
.= (id X) +* (((id Y) +* (f | X)) +* (f | Y)) by FUNCT_4:14
.= (id X) +* (((f | X) +* (id Y)) +* (f | Y)) by A4, Th1
.= (id X) +* ((f | X) +* ((id Y) +* (f | Y))) by FUNCT_4:14
.= (X -indexing f) +* (Y -indexing f) by FUNCT_4:14 ; :: thesis: verum