let p, q be Function; :: thesis: for A being set holds (p +* q) | A = (p | A) +* (q | A)
let A be set ; :: thesis: (p +* q) | A = (p | A) +* (q | A)
A1: dom ((p +* q) | A) = (dom (p +* q)) /\ A by RELAT_1:61
.= ((dom p) \/ (dom q)) /\ A by Def1
.= ((dom p) /\ A) \/ ((dom q) /\ A) by XBOOLE_1:23
.= (dom (p | A)) \/ ((dom q) /\ A) by RELAT_1:61
.= (dom (p | A)) \/ (dom (q | A)) by RELAT_1:61 ;
for x being object st x in (dom (p | A)) \/ (dom (q | A)) holds
( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) )
proof
let x be object ; :: thesis: ( x in (dom (p | A)) \/ (dom (q | A)) implies ( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) ) )
assume A2: x in (dom (p | A)) \/ (dom (q | A)) ; :: thesis: ( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) )
then ( x in dom (p | A) or x in dom (q | A) ) by XBOOLE_0:def 3;
then ( x in (dom p) /\ A or x in (dom q) /\ A ) by RELAT_1:61;
then A3: x in A by XBOOLE_0:def 4;
hereby :: thesis: ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x )
assume A4: x in dom (q | A) ; :: thesis: ((p +* q) | A) . x = (q | A) . x
then x in (dom q) /\ A by RELAT_1:61;
then A5: x in dom q by XBOOLE_0:def 4;
thus ((p +* q) | A) . x = (p +* q) . x by A1, A2, FUNCT_1:47
.= q . x by A5, Th13
.= (q | A) . x by A4, FUNCT_1:47 ; :: thesis: verum
end;
assume A6: not x in dom (q | A) ; :: thesis: ((p +* q) | A) . x = (p | A) . x
then not x in (dom q) /\ A by RELAT_1:61;
then A7: not x in dom q by A3, XBOOLE_0:def 4;
A8: x in dom (p | A) by A2, A6, XBOOLE_0:def 3;
then x in (dom p) /\ A by RELAT_1:61;
then x in dom p by XBOOLE_0:def 4;
then x in dom (p +* q) by Th12;
then x in (dom (p +* q)) /\ A by A3, XBOOLE_0:def 4;
then x in dom ((p +* q) | A) by RELAT_1:61;
hence ((p +* q) | A) . x = (p +* q) . x by FUNCT_1:47
.= p . x by A7, Th11
.= (p | A) . x by A8, FUNCT_1:47 ;
:: thesis: verum
end;
hence (p +* q) | A = (p | A) +* (q | A) by A1, Def1; :: thesis: verum