let U0 be Universal_Algebra; :: thesis: UniAlg_join U0 is commutative

set o = UniAlg_join U0;

for x, y being Element of Sub U0 holds (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x)

set o = UniAlg_join U0;

for x, y being Element of Sub U0 holds (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x)

proof

hence
UniAlg_join U0 is commutative
by BINOP_1:def 2; :: thesis: verum
let x, y be Element of Sub U0; :: thesis: (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x)

reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

reconsider B = the carrier of U1 \/ the carrier of U2 as non empty set ;

( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def7;

then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8;

A1: U1 "\/" U2 = GenUnivAlg B by Def13;

( (UniAlg_join U0) . (x,y) = U1 "\/" U2 & (UniAlg_join U0) . (y,x) = U2 "\/" U1 ) by Def15;

hence (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x) by A1, Def13; :: thesis: verum

end;reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

reconsider B = the carrier of U1 \/ the carrier of U2 as non empty set ;

( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def7;

then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8;

A1: U1 "\/" U2 = GenUnivAlg B by Def13;

( (UniAlg_join U0) . (x,y) = U1 "\/" U2 & (UniAlg_join U0) . (y,x) = U2 "\/" U1 ) by Def15;

hence (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x) by A1, Def13; :: thesis: verum