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:88;
f | X c= f by RELAT_1:88;
then f | X tolerates f | Y by A1, PARTFUN1:131;
then A2: (f | X) \/ (f | Y) = (f | X) +* (f | Y) by FUNCT_4:31;
dom (f | X) = (dom f) /\ X by RELAT_1:90;
then A3: dom (f | X) c= dom f by XBOOLE_1:17;
dom (f | Y) = (dom f) /\ Y by RELAT_1:90;
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:23
.= ((id X) +* (id Y)) +* ((f | X) +* (f | Y)) by A2, 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 A4, 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