let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)
let A1 be SetSequence of X; :: thesis: A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)

now

let n be Element of NAT ; :: thesis: (A (\+\) A1) . n = ((A (\) A1) (\/) (A1 (\) A)) . n
thus (A (\+\) A1) . n = A \+\ (A1 . n) by Def9
.= ((A (\) A1) . n) \/ ((A1 . n) \ A) by Def7
.= ((A (\) A1) . n) \/ ((A1 (\) A) . n) by Def8
.= ((A (\) A1) (\/) (A1 (\) A)) . n by Def2 ; :: thesis: verum

end;

hence A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A) by FUNCT_2:113; :: thesis: verum