let I be set ; :: thesis: for M being V8() ManySortedSet of
for X, Y being Element of M st X \/ Y is Element of M holds
(id M) .. (X \/ Y) = ((id M) .. X) \/ ((id M) .. Y)
let M be V8() ManySortedSet of ; :: thesis: for X, Y being Element of M st X \/ Y is Element of M holds
(id M) .. (X \/ Y) = ((id M) .. X) \/ ((id M) .. Y)
let X, Y be Element of M; :: thesis: ( X \/ Y is Element of M implies (id M) .. (X \/ Y) = ((id M) .. X) \/ ((id M) .. Y) )
set F = id M;
assume X \/ Y is Element of M ; :: thesis: (id M) .. (X \/ Y) = ((id M) .. X) \/ ((id M) .. Y)
hence (id M) .. (X \/ Y) = X \/ Y by Th8
.= ((id M) .. X) \/ Y by Th8
.= ((id M) .. X) \/ ((id M) .. Y) by Th8 ;
:: thesis: verum