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

now

let n be Element of NAT ; :: thesis: (A1 (\+\) A2) . n = ((A1 (\) A2) (\/) (A2 (\) A1)) . n
thus (A1 (\+\) A2) . n = (A1 . n) \+\ (A2 . n) by Def4
.= ((A1 (\) A2) . n) \/ ((A2 . n) \ (A1 . n)) by Def3
.= ((A1 (\) A2) . n) \/ ((A2 (\) A1) . n) by Def3
.= ((A1 (\) A2) (\/) (A2 (\) A1)) . n by Def2 ; :: thesis: verum

end;

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