let X, Y be set ; :: thesis: (id X) +* (id Y) = id (X \/ Y)
A1: for x being object st x in dom (id (X \/ Y)) holds
((id X) +* (id Y)) . x = (id (X \/ Y)) . x

proof

let x be object ; :: thesis: ( x in dom (id (X \/ Y)) implies ((id X) +* (id Y)) . x = (id (X \/ Y)) . x )
assume A2: x in dom (id (X \/ Y)) ; :: thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x

now :: thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x

per cases ( x in Y or not x in Y ) ;

suppose A3: x in Y ; :: thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x

dom (id Y) = Y ;
hence ((id X) +* (id Y)) . x = (id Y) . x by A3, Th13
.= x by A3, FUNCT_1:18
.= (id (X \/ Y)) . x by A2, FUNCT_1:18 ;
:: thesis: verum

end;

suppose A4: not x in Y ; :: thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x

then A5: x in X by A2, XBOOLE_0:def 3;
not x in dom (id Y) by A4;
hence ((id X) +* (id Y)) . x = (id X) . x by Th11
.= x by A5, FUNCT_1:18
.= (id (X \/ Y)) . x by A2, FUNCT_1:18 ;
:: thesis: verum

end;

end;

end;

hence ((id X) +* (id Y)) . x = (id (X \/ Y)) . x ; :: thesis: verum

end;

dom ((id X) +* (id Y)) = (dom (id X)) \/ (dom (id Y)) by Def1
.= X \/ (dom (id Y))
.= X \/ Y
.= dom (id (X \/ Y)) ;
hence (id X) +* (id Y) = id (X \/ Y) by A1; :: thesis: verum