let C, D be non empty set ; :: thesis: for B1, B2 being Element of Fin C

for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds

F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

let B1, B2 be Element of Fin C; :: thesis: for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds

F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

let F be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds

F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

let f be Function of C,D; :: thesis: ( F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 implies F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) )

assume that

A1: ( F is commutative & F is associative ) and

A2: ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) and

A3: B1 /\ B2 = {} ; :: according to XBOOLE_0:def 7 :: thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds

F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

let B1, B2 be Element of Fin C; :: thesis: for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds

F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

let F be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds

F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

let f be Function of C,D; :: thesis: ( F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 implies F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) )

assume that

A1: ( F is commutative & F is associative ) and

A2: ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) and

A3: B1 /\ B2 = {} ; :: according to XBOOLE_0:def 7 :: thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

now :: thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))end;

hence
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
; :: thesis: verumper cases
( B1 = {} or B2 = {} or ( B1 <> {} & B2 <> {} ) )
;

end;

suppose A4:
( B1 = {} or B2 = {} )
; :: thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

end;

now :: thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))end;

hence
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
; :: thesis: verumper cases
( B1 = {} or B2 = {} )
by A4;

end;

suppose A5:
B1 = {}
; :: thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

hence F $$ ((B1 \/ B2),f) =
F . ((the_unity_wrt F),(F $$ (B2,f)))
by A2, SETWISEO:15

.= F . ((F $$ (({}. C),f)),(F $$ (B2,f))) by A1, A2, A4, SETWISEO:31

.= F . ((F $$ (B1,f)),(F $$ (B2,f))) by A5 ;

:: thesis: verum

end;.= F . ((F $$ (({}. C),f)),(F $$ (B2,f))) by A1, A2, A4, SETWISEO:31

.= F . ((F $$ (B1,f)),(F $$ (B2,f))) by A5 ;

:: thesis: verum

suppose A6:
B2 = {}
; :: thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

hence F $$ ((B1 \/ B2),f) =
F . ((F $$ (B1,f)),(the_unity_wrt F))
by A2, SETWISEO:15

.= F . ((F $$ (B1,f)),(F $$ (({}. C),f))) by A1, A2, A4, SETWISEO:31

.= F . ((F $$ (B1,f)),(F $$ (B2,f))) by A6 ;

:: thesis: verum

end;.= F . ((F $$ (B1,f)),(F $$ (({}. C),f))) by A1, A2, A4, SETWISEO:31

.= F . ((F $$ (B1,f)),(F $$ (B2,f))) by A6 ;

:: thesis: verum

suppose A7:
( B1 <> {} & B2 <> {} )
; :: thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

defpred S_{1}[ Element of Fin C] means ( $1 <> {} & B1 /\ $1 = {} implies F $$ ((B1 \/ $1),f) = F . ((F $$ (B1,f)),(F $$ ($1,f))) );

A8: for B9 being Element of Fin C

for b being Element of C st S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {.b.}]
_{1}[ {}. C]
;

for B2 being Element of Fin C holds S_{1}[B2]
from SETWISEO:sch 2(A18, A8);

hence F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) by A3, A7; :: thesis: verum

end;A8: for B9 being Element of Fin C

for b being Element of C st S

S

proof

A18:
S
let B be Element of Fin C; :: thesis: for b being Element of C st S_{1}[B] & not b in B holds

S_{1}[B \/ {.b.}]

let c be Element of C; :: thesis: ( S_{1}[B] & not c in B implies S_{1}[B \/ {.c.}] )

assume that

A9: ( B <> {} & B1 /\ B = {} implies F $$ ((B1 \/ B),f) = F . ((F $$ (B1,f)),(F $$ (B,f))) ) and

A10: not c in B and

B \/ {c} <> {} ; :: thesis: ( not B1 /\ (B \/ {.c.}) = {} or F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) )

assume A11: B1 /\ (B \/ {c}) = {} ; :: thesis: F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))

then A12: B1 misses B \/ {c} ;

c in B \/ {c} by ZFMISC_1:136;

then A13: not c in B1 by A11, XBOOLE_0:def 4;

A14: ( B <> {} & B1 misses B implies F $$ ((B1 \/ B),f) = F . ((F $$ (B1,f)),(F $$ (B,f))) ) by A9;

end;S

let c be Element of C; :: thesis: ( S

assume that

A9: ( B <> {} & B1 /\ B = {} implies F $$ ((B1 \/ B),f) = F . ((F $$ (B1,f)),(F $$ (B,f))) ) and

A10: not c in B and

B \/ {c} <> {} ; :: thesis: ( not B1 /\ (B \/ {.c.}) = {} or F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) )

assume A11: B1 /\ (B \/ {c}) = {} ; :: thesis: F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))

then A12: B1 misses B \/ {c} ;

c in B \/ {c} by ZFMISC_1:136;

then A13: not c in B1 by A11, XBOOLE_0:def 4;

A14: ( B <> {} & B1 misses B implies F $$ ((B1 \/ B),f) = F . ((F $$ (B1,f)),(F $$ (B,f))) ) by A9;

now :: thesis: F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))end;

hence
F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))
; :: thesis: verumper cases
( B = {} or B <> {} )
;

end;

suppose A15:
B = {}
; :: thesis: F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))

hence F $$ ((B1 \/ (B \/ {.c.})),f) =
F . ((F $$ (B1,f)),(f . c))
by A1, A7, A13, Th2

.= F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) by A1, A15, SETWISEO:17 ;

:: thesis: verum

end;.= F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) by A1, A15, SETWISEO:17 ;

:: thesis: verum

suppose A16:
B <> {}
; :: thesis: F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))

A17:
not c in B1 \/ B
by A10, A13, XBOOLE_0:def 3;

thus F $$ ((B1 \/ (B \/ {.c.})),f) = F $$ (((B1 \/ B) \/ {.c.}),f) by XBOOLE_1:4

.= F . ((F . ((F $$ (B1,f)),(F $$ (B,f)))),(f . c)) by A1, A14, A12, A16, A17, Th2, XBOOLE_1:7, XBOOLE_1:63

.= F . ((F $$ (B1,f)),(F . ((F $$ (B,f)),(f . c)))) by A1

.= F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) by A1, A10, A16, Th2 ; :: thesis: verum

end;thus F $$ ((B1 \/ (B \/ {.c.})),f) = F $$ (((B1 \/ B) \/ {.c.}),f) by XBOOLE_1:4

.= F . ((F . ((F $$ (B1,f)),(F $$ (B,f)))),(f . c)) by A1, A14, A12, A16, A17, Th2, XBOOLE_1:7, XBOOLE_1:63

.= F . ((F $$ (B1,f)),(F . ((F $$ (B,f)),(f . c)))) by A1

.= F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) by A1, A10, A16, Th2 ; :: thesis: verum

for B2 being Element of Fin C holds S

hence F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) by A3, A7; :: thesis: verum