let f, g be 1-sorted-yielding Function; :: thesis: Carrier (f +* g) = (Carrier f) +* (Carrier g)
A1: dom (Carrier (f +* g)) = dom (f +* g) by Def13
.= (dom f) \/ (dom g) by FUNCT_4:def 1 ;
then A2: dom (Carrier (f +* g)) = (dom (Carrier f)) \/ (dom g) by Def13
.= (dom (Carrier f)) \/ (dom (Carrier g)) by Def13
.= dom ((Carrier f) +* (Carrier g)) by FUNCT_4:def 1 ;

now :: thesis: for x being object st x in dom (Carrier (f +* g)) holds
(Carrier (f +* g)) . x = ((Carrier f) +* (Carrier g)) . x

let x be object ; :: thesis: ( x in dom (Carrier (f +* g)) implies (Carrier (f +* g)) . b₁ = ((Carrier f) +* (Carrier g)) . b₁ )
assume x in dom (Carrier (f +* g)) ; :: thesis: (Carrier (f +* g)) . b₁ = ((Carrier f) +* (Carrier g)) . b₁
then A3: ( x in (dom f) \/ (dom g) & x is set ) by A1;
then x in dom (f +* g) by FUNCT_4:def 1;
then consider R being 1-sorted such that
A4: ( R = (f +* g) . x & (Carrier (f +* g)) . x = the carrier of R ) by Def13;

per cases ( x in dom g or not x in dom g ) ;

suppose A5: x in dom g ; :: thesis: (Carrier (f +* g)) . b₁ = ((Carrier f) +* (Carrier g)) . b₁

then consider R9 being 1-sorted such that
A6: ( R9 = g . x & (Carrier g) . x = the carrier of R9 ) by Def13;
( R = R9 & x in dom (Carrier g) ) by A4, A5, A6, FUNCT_4:13, Def13;
hence (Carrier (f +* g)) . x = ((Carrier f) +* (Carrier g)) . x by A4, A6, FUNCT_4:13; :: thesis: verum

end;

suppose A8: not x in dom g ; :: thesis: (Carrier (f +* g)) . b₁ = ((Carrier f) +* (Carrier g)) . b₁

then A9: ( not x in dom (Carrier g) & x in dom f ) by A3, XBOOLE_0:def 3, Def13;
then consider R9 being 1-sorted such that
A10: ( R9 = f . x & (Carrier f) . x = the carrier of R9 ) by Def13;
R = R9 by A4, A8, A10, FUNCT_4:11;
hence (Carrier (f +* g)) . x = ((Carrier f) +* (Carrier g)) . x by A4, A9, A10, FUNCT_4:11; :: thesis: verum

end;

end;

end;

hence Carrier (f +* g) = (Carrier f) +* (Carrier g) by A2; :: thesis: verum