:: BINOP_1 semantic presentation begin definition let f be Function; let a, b be set ; funcf . (a,b) -> set equals :: BINOP_1:def 1 f . [a,b]; correctness coherence f . [a,b] is set ; ; end; :: deftheorem defines . BINOP_1:def_1_:_ for f being Function for a, b being set holds f . (a,b) = f . [a,b]; definition let A, B be non empty set ; let C be set ; let f be Function of [:A,B:],C; let a be Element of A; let b be Element of B; :: original: . redefine funcf . (a,b) -> Element of C; coherence f . (a,b) is Element of C proof reconsider ab = [a,b] as Element of [:A,B:] by ZFMISC_1:def_2; f . ab is Element of C ; hence f . (a,b) is Element of C ; ::_thesis: verum end; end; theorem Th1: :: BINOP_1:1 for X, Y, Z being set for f1, f2 being Function of [:X,Y:],Z st ( for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) ) holds f1 = f2 proof let X, Y, Z be set ; ::_thesis: for f1, f2 being Function of [:X,Y:],Z st ( for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) ) holds f1 = f2 let f1, f2 be Function of [:X,Y:],Z; ::_thesis: ( ( for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) ) implies f1 = f2 ) assume A1: for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) ; ::_thesis: f1 = f2 for z being set st z in [:X,Y:] holds f1 . z = f2 . z proof let z be set ; ::_thesis: ( z in [:X,Y:] implies f1 . z = f2 . z ) assume z in [:X,Y:] ; ::_thesis: f1 . z = f2 . z then consider x, y being set such that A2: ( x in X & y in Y ) and A3: z = [x,y] by ZFMISC_1:def_2; ( f1 . (x,y) = f1 . z & f2 . (x,y) = f2 . z ) by A3; hence f1 . z = f2 . z by A1, A2; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:12; ::_thesis: verum end; theorem :: BINOP_1:2 for X, Y, Z being set for f1, f2 being Function of [:X,Y:],Z st ( for a being Element of X for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ) holds f1 = f2 proof let X, Y, Z be set ; ::_thesis: for f1, f2 being Function of [:X,Y:],Z st ( for a being Element of X for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ) holds f1 = f2 let f1, f2 be Function of [:X,Y:],Z; ::_thesis: ( ( for a being Element of X for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ) implies f1 = f2 ) assume for a being Element of X for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ; ::_thesis: f1 = f2 then for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) ; hence f1 = f2 by Th1; ::_thesis: verum end; definition let A be set ; mode UnOp of A is Function of A,A; mode BinOp of A is Function of [:A,A:],A; end; definition let A be set ; let f be BinOp of A; let a, b be Element of A; :: original: . redefine funcf . (a,b) -> Element of A; coherence f . (a,b) is Element of A proof percases ( A <> {} or A = {} ) ; suppose A <> {} ; ::_thesis: f . (a,b) is Element of A then reconsider A = A as non empty set ; reconsider f = f as BinOp of A ; reconsider ab = [a,b] as Element of [:A,A:] by ZFMISC_1:def_2; f . ab is Element of A ; hence f . (a,b) is Element of A ; ::_thesis: verum end; supposeA1: A = {} ; ::_thesis: f . (a,b) is Element of A then not [a,b] in dom f ; then f . (a,b) = {} by FUNCT_1:def_2; hence f . (a,b) is Element of A by A1, SUBSET_1:def_1; ::_thesis: verum end; end; end; end; scheme :: BINOP_1:sch 1 FuncEx2{ F1() -> set , F2() -> set , F3() -> set , P1[ set , set , set ] } : ex f being Function of [:F1(),F2():],F3() st for x, y being set st x in F1() & y in F2() holds P1[x,y,f . (x,y)] provided A1: for x, y being set st x in F1() & y in F2() holds ex z being set st ( z in F3() & P1[x,y,z] ) proof defpred S1[ set , set ] means for x1, y1 being set st \$1 = [x1,y1] holds P1[x1,y1,\$2]; A2: for x being set st x in [:F1(),F2():] holds ex z being set st ( z in F3() & S1[x,z] ) proof let x be set ; ::_thesis: ( x in [:F1(),F2():] implies ex z being set st ( z in F3() & S1[x,z] ) ) assume x in [:F1(),F2():] ; ::_thesis: ex z being set st ( z in F3() & S1[x,z] ) then consider x1, y1 being set such that A3: ( x1 in F1() & y1 in F2() ) and A4: x = [x1,y1] by ZFMISC_1:def_2; consider z being set such that A5: z in F3() and A6: P1[x1,y1,z] by A1, A3; take z ; ::_thesis: ( z in F3() & S1[x,z] ) thus z in F3() by A5; ::_thesis: S1[x,z] let x2, y2 be set ; ::_thesis: ( x = [x2,y2] implies P1[x2,y2,z] ) assume A7: x = [x2,y2] ; ::_thesis: P1[x2,y2,z] then x1 = x2 by A4, XTUPLE_0:1; hence P1[x2,y2,z] by A4, A6, A7, XTUPLE_0:1; ::_thesis: verum end; consider f being Function of [:F1(),F2():],F3() such that A8: for x being set st x in [:F1(),F2():] holds S1[x,f . x] from FUNCT_2:sch_1(A2); take f ; ::_thesis: for x, y being set st x in F1() & y in F2() holds P1[x,y,f . (x,y)] let x, y be set ; ::_thesis: ( x in F1() & y in F2() implies P1[x,y,f . (x,y)] ) assume ( x in F1() & y in F2() ) ; ::_thesis: P1[x,y,f . (x,y)] then [x,y] in [:F1(),F2():] by ZFMISC_1:def_2; hence P1[x,y,f . (x,y)] by A8; ::_thesis: verum end; scheme :: BINOP_1:sch 2 Lambda2{ F1() -> set , F2() -> set , F3() -> set , F4( set , set ) -> set } : ex f being Function of [:F1(),F2():],F3() st for x, y being set st x in F1() & y in F2() holds f . (x,y) = F4(x,y) provided A1: for x, y being set st x in F1() & y in F2() holds F4(x,y) in F3() proof defpred S1[ set , set , set ] means \$3 = F4(\$1,\$2); A2: for x, y being set st x in F1() & y in F2() holds ex z being set st ( z in F3() & S1[x,y,z] ) by A1; thus ex f being Function of [:F1(),F2():],F3() st for x, y being set st x in F1() & y in F2() holds S1[x,y,f . (x,y)] from BINOP_1:sch_1(A2); ::_thesis: verum end; scheme :: BINOP_1:sch 3 FuncEx2D{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set , set ] } : ex f being Function of [:F1(),F2():],F3() st for x being Element of F1() for y being Element of F2() holds P1[x,y,f . (x,y)] provided A1: for x being Element of F1() for y being Element of F2() ex z being Element of F3() st P1[x,y,z] proof defpred S1[ set , set ] means for x being Element of F1() for y being Element of F2() st \$1 = [x,y] holds P1[x,y,\$2]; A2: for p being Element of [:F1(),F2():] ex z being Element of F3() st S1[p,z] proof let p be Element of [:F1(),F2():]; ::_thesis: ex z being Element of F3() st S1[p,z] consider x1, y1 being set such that A3: x1 in F1() and A4: y1 in F2() and A5: p = [x1,y1] by ZFMISC_1:def_2; reconsider y1 = y1 as Element of F2() by A4; reconsider x1 = x1 as Element of F1() by A3; consider z being Element of F3() such that A6: P1[x1,y1,z] by A1; take z ; ::_thesis: S1[p,z] let x be Element of F1(); ::_thesis: for y being Element of F2() st p = [x,y] holds P1[x,y,z] let y be Element of F2(); ::_thesis: ( p = [x,y] implies P1[x,y,z] ) assume A7: p = [x,y] ; ::_thesis: P1[x,y,z] then x1 = x by A5, XTUPLE_0:1; hence P1[x,y,z] by A5, A6, A7, XTUPLE_0:1; ::_thesis: verum end; consider f being Function of [:F1(),F2():],F3() such that A8: for p being Element of [:F1(),F2():] holds S1[p,f . p] from FUNCT_2:sch_3(A2); take f ; ::_thesis: for x being Element of F1() for y being Element of F2() holds P1[x,y,f . (x,y)] let x be Element of F1(); ::_thesis: for y being Element of F2() holds P1[x,y,f . (x,y)] let y be Element of F2(); ::_thesis: P1[x,y,f . (x,y)] reconsider xy = [x,y] as Element of [:F1(),F2():] by ZFMISC_1:def_2; P1[x,y,f . xy] by A8; hence P1[x,y,f . (x,y)] ; ::_thesis: verum end; scheme :: BINOP_1:sch 4 Lambda2D{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( Element of F1(), Element of F2()) -> Element of F3() } : ex f being Function of [:F1(),F2():],F3() st for x being Element of F1() for y being Element of F2() holds f . (x,y) = F4(x,y) proof defpred S1[ Element of F1(), Element of F2(), set ] means \$3 = F4(\$1,\$2); A1: for x being Element of F1() for y being Element of F2() ex z being Element of F3() st S1[x,y,z] ; thus ex f being Function of [:F1(),F2():],F3() st for x being Element of F1() for y being Element of F2() holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1); ::_thesis: verum end; definition let A be set ; let o be BinOp of A; attro is commutative means :Def2: :: BINOP_1:def 2 for a, b being Element of A holds o . (a,b) = o . (b,a); attro is associative means :: BINOP_1:def 3 for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c); attro is idempotent means :: BINOP_1:def 4 for a being Element of A holds o . (a,a) = a; end; :: deftheorem Def2 defines commutative BINOP_1:def_2_:_ for A being set for o being BinOp of A holds ( o is commutative iff for a, b being Element of A holds o . (a,b) = o . (b,a) ); :: deftheorem defines associative BINOP_1:def_3_:_ for A being set for o being BinOp of A holds ( o is associative iff for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c) ); :: deftheorem defines idempotent BINOP_1:def_4_:_ for A being set for o being BinOp of A holds ( o is idempotent iff for a being Element of A holds o . (a,a) = a ); registration cluster Function-like V18([:{},{}:], {} ) -> empty commutative associative for Element of bool [:[:{},{}:],{}:]; coherence for b1 being BinOp of {} holds ( b1 is empty & b1 is associative & b1 is commutative ) proof let f be BinOp of {}; ::_thesis: ( f is empty & f is associative & f is commutative ) thus f is empty ; ::_thesis: ( f is associative & f is commutative ) A1: f c= [:(dom f),(rng f):] ; hereby :: according to BINOP_1:def_3 ::_thesis: f is commutative let a, b, c be Element of {} ; ::_thesis: f . (a,(f . (b,c))) = f . ((f . (a,b)),c) thus f . (a,(f . (b,c))) = {} by A1, FUNCT_1:def_2 .= f . ((f . (a,b)),c) by A1, FUNCT_1:def_2 ; ::_thesis: verum end; let a, b be Element of {} ; :: according to BINOP_1:def_2 ::_thesis: f . (a,b) = f . (b,a) thus f . (a,b) = {} by A1, FUNCT_1:def_2 .= f . (b,a) by A1, FUNCT_1:def_2 ; ::_thesis: verum end; end; definition let A be set ; let e be Element of A; let o be BinOp of A; prede is_a_left_unity_wrt o means :Def5: :: BINOP_1:def 5 for a being Element of A holds o . (e,a) = a; prede is_a_right_unity_wrt o means :Def6: :: BINOP_1:def 6 for a being Element of A holds o . (a,e) = a; end; :: deftheorem Def5 defines is_a_left_unity_wrt BINOP_1:def_5_:_ for A being set for e being Element of A for o being BinOp of A holds ( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a ); :: deftheorem Def6 defines is_a_right_unity_wrt BINOP_1:def_6_:_ for A being set for e being Element of A for o being BinOp of A holds ( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a ); definition let A be set ; let e be Element of A; let o be BinOp of A; prede is_a_unity_wrt o means :: BINOP_1:def 7 ( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o ); end; :: deftheorem defines is_a_unity_wrt BINOP_1:def_7_:_ for A being set for e being Element of A for o being BinOp of A holds ( e is_a_unity_wrt o iff ( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o ) ); theorem Th3: :: BINOP_1:3 for A being set for o being BinOp of A for e being Element of A holds ( e is_a_unity_wrt o iff for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) proof let A be set ; ::_thesis: for o being BinOp of A for e being Element of A holds ( e is_a_unity_wrt o iff for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) let o be BinOp of A; ::_thesis: for e being Element of A holds ( e is_a_unity_wrt o iff for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) let e be Element of A; ::_thesis: ( e is_a_unity_wrt o iff for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) thus ( e is_a_unity_wrt o implies for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) ::_thesis: ( ( for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) implies e is_a_unity_wrt o ) proof assume ( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o ) ; :: according to BINOP_1:def_7 ::_thesis: for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) hence for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) by Def5, Def6; ::_thesis: verum end; assume for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ; ::_thesis: e is_a_unity_wrt o hence ( ( for a being Element of A holds o . (e,a) = a ) & ( for a being Element of A holds o . (a,e) = a ) ) ; :: according to BINOP_1:def_5,BINOP_1:def_6,BINOP_1:def_7 ::_thesis: verum end; theorem Th4: :: BINOP_1:4 for A being set for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) proof let A be set ; ::_thesis: for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) let o be BinOp of A; ::_thesis: for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) ) assume A1: o is commutative ; ::_thesis: ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) now__::_thesis:_(_(_(_for_a_being_Element_of_A_holds_ (_o_._(e,a)_=_a_&_o_._(a,e)_=_a_)_)_implies_for_a_being_Element_of_A_holds_o_._(e,a)_=_a_)_&_(_(_for_a_being_Element_of_A_holds_o_._(e,a)_=_a_)_implies_for_a_being_Element_of_A_holds_ (_o_._(e,a)_=_a_&_o_._(a,e)_=_a_)_)_) thus ( ( for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) implies for a being Element of A holds o . (e,a) = a ) ; ::_thesis: ( ( for a being Element of A holds o . (e,a) = a ) implies for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) assume A2: for a being Element of A holds o . (e,a) = a ; ::_thesis: for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) let a be Element of A; ::_thesis: ( o . (e,a) = a & o . (a,e) = a ) thus o . (e,a) = a by A2; ::_thesis: o . (a,e) = a thus o . (a,e) = o . (e,a) by A1, Def2 .= a by A2 ; ::_thesis: verum end; hence ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) by Th3; ::_thesis: verum end; theorem Th5: :: BINOP_1:5 for A being set for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) proof let A be set ; ::_thesis: for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) let o be BinOp of A; ::_thesis: for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) ) assume A1: o is commutative ; ::_thesis: ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) now__::_thesis:_(_(_(_for_a_being_Element_of_A_holds_ (_o_._(e,a)_=_a_&_o_._(a,e)_=_a_)_)_implies_for_a_being_Element_of_A_holds_o_._(a,e)_=_a_)_&_(_(_for_a_being_Element_of_A_holds_o_._(a,e)_=_a_)_implies_for_a_being_Element_of_A_holds_ (_o_._(e,a)_=_a_&_o_._(a,e)_=_a_)_)_) thus ( ( for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) implies for a being Element of A holds o . (a,e) = a ) ; ::_thesis: ( ( for a being Element of A holds o . (a,e) = a ) implies for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) ) assume A2: for a being Element of A holds o . (a,e) = a ; ::_thesis: for a being Element of A holds ( o . (e,a) = a & o . (a,e) = a ) let a be Element of A; ::_thesis: ( o . (e,a) = a & o . (a,e) = a ) thus o . (e,a) = o . (a,e) by A1, Def2 .= a by A2 ; ::_thesis: o . (a,e) = a thus o . (a,e) = a by A2; ::_thesis: verum end; hence ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) by Th3; ::_thesis: verum end; theorem Th6: :: BINOP_1:6 for A being set for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) proof let A be set ; ::_thesis: for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) let o be BinOp of A; ::_thesis: for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) ) ( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) by Def5; hence ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) ) by Th4; ::_thesis: verum end; theorem Th7: :: BINOP_1:7 for A being set for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff e is_a_right_unity_wrt o ) proof let A be set ; ::_thesis: for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff e is_a_right_unity_wrt o ) let o be BinOp of A; ::_thesis: for e being Element of A st o is commutative holds ( e is_a_unity_wrt o iff e is_a_right_unity_wrt o ) let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_right_unity_wrt o ) ) ( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) by Def6; hence ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_right_unity_wrt o ) ) by Th5; ::_thesis: verum end; theorem :: BINOP_1:8 for A being set for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) proof let A be set ; ::_thesis: for o being BinOp of A for e being Element of A st o is commutative holds ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) let o be BinOp of A; ::_thesis: for e being Element of A st o is commutative holds ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) ) assume A1: o is commutative ; ::_thesis: ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) then ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) by Th6; hence ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) by A1, Th7; ::_thesis: verum end; theorem Th9: :: BINOP_1:9 for A being set for o being BinOp of A for e1, e2 being Element of A st e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o holds e1 = e2 proof let A be set ; ::_thesis: for o being BinOp of A for e1, e2 being Element of A st e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o holds e1 = e2 let o be BinOp of A; ::_thesis: for e1, e2 being Element of A st e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o holds e1 = e2 let e1, e2 be Element of A; ::_thesis: ( e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o implies e1 = e2 ) assume that A1: e1 is_a_left_unity_wrt o and A2: e2 is_a_right_unity_wrt o ; ::_thesis: e1 = e2 thus e1 = o . (e1,e2) by A2, Def6 .= e2 by A1, Def5 ; ::_thesis: verum end; theorem Th10: :: BINOP_1:10 for A being set for o being BinOp of A for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds e1 = e2 proof let A be set ; ::_thesis: for o being BinOp of A for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds e1 = e2 let o be BinOp of A; ::_thesis: for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds e1 = e2 let e1, e2 be Element of A; ::_thesis: ( e1 is_a_unity_wrt o & e2 is_a_unity_wrt o implies e1 = e2 ) assume that e1 is_a_left_unity_wrt o and A1: ( e1 is_a_right_unity_wrt o & e2 is_a_left_unity_wrt o ) and e2 is_a_right_unity_wrt o ; :: according to BINOP_1:def_7 ::_thesis: e1 = e2 thus e1 = e2 by A1, Th9; ::_thesis: verum end; definition let A be set ; let o be BinOp of A; assume A1: ex e being Element of A st e is_a_unity_wrt o ; func the_unity_wrt o -> Element of A means :: BINOP_1:def 8 it is_a_unity_wrt o; existence ex b1 being Element of A st b1 is_a_unity_wrt o by A1; uniqueness for b1, b2 being Element of A st b1 is_a_unity_wrt o & b2 is_a_unity_wrt o holds b1 = b2 by Th10; end; :: deftheorem defines the_unity_wrt BINOP_1:def_8_:_ for A being set for o being BinOp of A st ex e being Element of A st e is_a_unity_wrt o holds for b3 being Element of A holds ( b3 = the_unity_wrt o iff b3 is_a_unity_wrt o ); definition let A be set ; let o9, o be BinOp of A; predo9 is_left_distributive_wrt o means :Def9: :: BINOP_1:def 9 for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))); predo9 is_right_distributive_wrt o means :Def10: :: BINOP_1:def 10 for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))); end; :: deftheorem Def9 defines is_left_distributive_wrt BINOP_1:def_9_:_ for A being set for o9, o being BinOp of A holds ( o9 is_left_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ); :: deftheorem Def10 defines is_right_distributive_wrt BINOP_1:def_10_:_ for A being set for o9, o being BinOp of A holds ( o9 is_right_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ); definition let A be set ; let o9, o be BinOp of A; predo9 is_distributive_wrt o means :: BINOP_1:def 11 ( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o ); end; :: deftheorem defines is_distributive_wrt BINOP_1:def_11_:_ for A being set for o9, o being BinOp of A holds ( o9 is_distributive_wrt o iff ( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o ) ); theorem Th11: :: BINOP_1:11 for A being set for o9, o being BinOp of A holds ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) proof let A be set ; ::_thesis: for o9, o being BinOp of A holds ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) let o9, o be BinOp of A; ::_thesis: ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) thus ( o9 is_distributive_wrt o implies for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) ::_thesis: ( ( for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) implies o9 is_distributive_wrt o ) proof assume ( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o ) ; :: according to BINOP_1:def_11 ::_thesis: for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) hence for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) by Def9, Def10; ::_thesis: verum end; assume for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ; ::_thesis: o9 is_distributive_wrt o hence ( ( for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) & ( for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) ; :: according to BINOP_1:def_9,BINOP_1:def_10,BINOP_1:def_11 ::_thesis: verum end; theorem Th12: :: BINOP_1:12 for A being non empty set for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) proof let A be non empty set ; ::_thesis: for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) let o, o9 be BinOp of A; ::_thesis: ( o9 is commutative implies ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) ) assume A1: o9 is commutative ; ::_thesis: ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) ( ( for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) proof thus ( ( for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) implies for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) ; ::_thesis: ( ( for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) implies for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) assume A2: for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ; ::_thesis: for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) let a, b, c be Element of A; ::_thesis: ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) thus o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) by A2; ::_thesis: o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) thus o9 . ((o . (a,b)),c) = o9 . (c,(o . (a,b))) by A1, Def2 .= o . ((o9 . (c,a)),(o9 . (c,b))) by A2 .= o . ((o9 . (a,c)),(o9 . (c,b))) by A1, Def2 .= o . ((o9 . (a,c)),(o9 . (b,c))) by A1, Def2 ; ::_thesis: verum end; hence ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) by Th11; ::_thesis: verum end; theorem Th13: :: BINOP_1:13 for A being non empty set for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) proof let A be non empty set ; ::_thesis: for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) let o, o9 be BinOp of A; ::_thesis: ( o9 is commutative implies ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) assume A1: o9 is commutative ; ::_thesis: ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ( ( for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) proof thus ( ( for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) implies for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ; ::_thesis: ( ( for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) implies for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) assume A2: for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ; ::_thesis: for a, b, c being Element of A holds ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) let a, b, c be Element of A; ::_thesis: ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) thus o9 . (a,(o . (b,c))) = o9 . ((o . (b,c)),a) by A1, Def2 .= o . ((o9 . (b,a)),(o9 . (c,a))) by A2 .= o . ((o9 . (a,b)),(o9 . (c,a))) by A1, Def2 .= o . ((o9 . (a,b)),(o9 . (a,c))) by A1, Def2 ; ::_thesis: o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) thus o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) by A2; ::_thesis: verum end; hence ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) by Th11; ::_thesis: verum end; theorem Th14: :: BINOP_1:14 for A being non empty set for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) proof let A be non empty set ; ::_thesis: for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) let o, o9 be BinOp of A; ::_thesis: ( o9 is commutative implies ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) ) ( o9 is_left_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) by Def9; hence ( o9 is commutative implies ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) ) by Th12; ::_thesis: verum end; theorem Th15: :: BINOP_1:15 for A being non empty set for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o ) proof let A be non empty set ; ::_thesis: for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o ) let o, o9 be BinOp of A; ::_thesis: ( o9 is commutative implies ( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o ) ) ( o9 is_right_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) by Def10; hence ( o9 is commutative implies ( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o ) ) by Th13; ::_thesis: verum end; theorem :: BINOP_1:16 for A being non empty set for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) proof let A be non empty set ; ::_thesis: for o, o9 being BinOp of A st o9 is commutative holds ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) let o, o9 be BinOp of A; ::_thesis: ( o9 is commutative implies ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) ) assume A1: o9 is commutative ; ::_thesis: ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) then ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) by Th14; hence ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) by A1, Th15; ::_thesis: verum end; definition let A be set ; let u be UnOp of A; let o be BinOp of A; predu is_distributive_wrt o means :Def12: :: BINOP_1:def 12 for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)); end; :: deftheorem Def12 defines is_distributive_wrt BINOP_1:def_12_:_ for A being set for u being UnOp of A for o being BinOp of A holds ( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) ); definition canceled; canceled; canceled; let A be non empty set ; let e be Element of A; let o be BinOp of A; redefine pred e is_a_left_unity_wrt o means :: BINOP_1:def 16 for a being Element of A holds o . (e,a) = a; correctness compatibility ( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a ); by Def5; redefine pred e is_a_right_unity_wrt o means :: BINOP_1:def 17 for a being Element of A holds o . (a,e) = a; correctness compatibility ( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a ); by Def6; end; :: deftheorem BINOP_1:def_13_:_ canceled; :: deftheorem BINOP_1:def_14_:_ canceled; :: deftheorem BINOP_1:def_15_:_ canceled; :: deftheorem defines is_a_left_unity_wrt BINOP_1:def_16_:_ for A being non empty set for e being Element of A for o being BinOp of A holds ( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a ); :: deftheorem defines is_a_right_unity_wrt BINOP_1:def_17_:_ for A being non empty set for e being Element of A for o being BinOp of A holds ( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a ); definition let A be non empty set ; let o9, o be BinOp of A; redefine pred o9 is_left_distributive_wrt o means :: BINOP_1:def 18 for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))); correctness compatibility ( o9 is_left_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ); by Def9; redefine pred o9 is_right_distributive_wrt o means :: BINOP_1:def 19 for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))); correctness compatibility ( o9 is_right_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ); by Def10; end; :: deftheorem defines is_left_distributive_wrt BINOP_1:def_18_:_ for A being non empty set for o9, o being BinOp of A holds ( o9 is_left_distributive_wrt o iff for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ); :: deftheorem defines is_right_distributive_wrt BINOP_1:def_19_:_ for A being non empty set for o9, o being BinOp of A holds ( o9 is_right_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ); definition let A be non empty set ; let u be UnOp of A; let o be BinOp of A; redefine pred u is_distributive_wrt o means :: BINOP_1:def 20 for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)); correctness compatibility ( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) ); by Def12; end; :: deftheorem defines is_distributive_wrt BINOP_1:def_20_:_ for A being non empty set for u being UnOp of A for o being BinOp of A holds ( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) ); theorem :: BINOP_1:17 for X, Y, Z, x, y being set for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds f . (x,y) in Z proof let X, Y, Z, x, y be set ; ::_thesis: for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds f . (x,y) in Z let f be Function of [:X,Y:],Z; ::_thesis: ( x in X & y in Y & Z <> {} implies f . (x,y) in Z ) assume ( x in X & y in Y ) ; ::_thesis: ( not Z <> {} or f . (x,y) in Z ) then [x,y] in [:X,Y:] by ZFMISC_1:87; hence ( not Z <> {} or f . (x,y) in Z ) by FUNCT_2:5; ::_thesis: verum end; theorem :: BINOP_1:18 for x, y, X, Y, Z being set for f being Function of [:X,Y:],Z for g being Function st Z <> {} & x in X & y in Y holds (g * f) . (x,y) = g . (f . (x,y)) proof let x, y, X, Y, Z be set ; ::_thesis: for f being Function of [:X,Y:],Z for g being Function st Z <> {} & x in X & y in Y holds (g * f) . (x,y) = g . (f . (x,y)) let f be Function of [:X,Y:],Z; ::_thesis: for g being Function st Z <> {} & x in X & y in Y holds (g * f) . (x,y) = g . (f . (x,y)) let g be Function; ::_thesis: ( Z <> {} & x in X & y in Y implies (g * f) . (x,y) = g . (f . (x,y)) ) assume A1: Z <> {} ; ::_thesis: ( not x in X or not y in Y or (g * f) . (x,y) = g . (f . (x,y)) ) assume ( x in X & y in Y ) ; ::_thesis: (g * f) . (x,y) = g . (f . (x,y)) then [x,y] in [:X,Y:] by ZFMISC_1:87; hence (g * f) . (x,y) = g . (f . (x,y)) by A1, FUNCT_2:15; ::_thesis: verum end; theorem :: BINOP_1:19 for X, Y being set for f being Function st dom f = [:X,Y:] holds ( f is constant iff for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds f . (x1,y1) = f . (x2,y2) ) proof let X, Y be set ; ::_thesis: for f being Function st dom f = [:X,Y:] holds ( f is constant iff for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds f . (x1,y1) = f . (x2,y2) ) let f be Function; ::_thesis: ( dom f = [:X,Y:] implies ( f is constant iff for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds f . (x1,y1) = f . (x2,y2) ) ) assume A1: dom f = [:X,Y:] ; ::_thesis: ( f is constant iff for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds f . (x1,y1) = f . (x2,y2) ) hereby ::_thesis: ( ( for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds f . (x1,y1) = f . (x2,y2) ) implies f is constant ) assume A2: f is constant ; ::_thesis: for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds f . (x1,y1) = f . (x2,y2) let x1, x2, y1, y2 be set ; ::_thesis: ( x1 in X & x2 in X & y1 in Y & y2 in Y implies f . (x1,y1) = f . (x2,y2) ) assume ( x1 in X & x2 in X & y1 in Y & y2 in Y ) ; ::_thesis: f . (x1,y1) = f . (x2,y2) then ( [x1,y1] in [:X,Y:] & [x2,y2] in [:X,Y:] ) by ZFMISC_1:87; hence f . (x1,y1) = f . (x2,y2) by A1, A2, FUNCT_1:def_10; ::_thesis: verum end; assume A3: for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds f . (x1,y1) = f . (x2,y2) ; ::_thesis: f is constant let x be set ; :: according to FUNCT_1:def_10 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or f . x = f . b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or f . x = f . y ) assume x in dom f ; ::_thesis: ( not y in dom f or f . x = f . y ) then consider x1, y1 being set such that A4: ( x1 in X & y1 in Y ) and A5: x = [x1,y1] by A1, ZFMISC_1:84; assume y in dom f ; ::_thesis: f . x = f . y then consider x2, y2 being set such that A6: ( x2 in X & y2 in Y ) and A7: y = [x2,y2] by A1, ZFMISC_1:84; thus f . x = f . (x1,y1) by A5 .= f . (x2,y2) by A3, A4, A6 .= f . y by A7 ; ::_thesis: verum end; theorem :: BINOP_1:20 for X, Y, Z being set for f1, f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds f1 . (x,y) = f2 . (x,y) ) holds f1 = f2 proof let X, Y, Z be set ; ::_thesis: for f1, f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds f1 . (x,y) = f2 . (x,y) ) holds f1 = f2 let f1, f2 be PartFunc of [:X,Y:],Z; ::_thesis: ( dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds f1 . (x,y) = f2 . (x,y) ) implies f1 = f2 ) assume that A1: dom f1 = dom f2 and A2: for x, y being set st [x,y] in dom f1 holds f1 . (x,y) = f2 . (x,y) ; ::_thesis: f1 = f2 for z being set st z in dom f1 holds f1 . z = f2 . z proof let z be set ; ::_thesis: ( z in dom f1 implies f1 . z = f2 . z ) assume A3: z in dom f1 ; ::_thesis: f1 . z = f2 . z then consider x, y being set such that A4: z = [x,y] by RELAT_1:def_1; f1 . (x,y) = f2 . (x,y) by A2, A3, A4; hence f1 . z = f2 . z by A4; ::_thesis: verum end; hence f1 = f2 by A1, FUNCT_1:2; ::_thesis: verum end; scheme :: BINOP_1:sch 5 PartFuncEx2{ F1() -> set , F2() -> set , F3() -> set , P1[ set , set , set ] } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) ) & ( for x, y being set st [x,y] in dom f holds P1[x,y,f . (x,y)] ) ) provided A1: for x, y, z being set st x in F1() & y in F2() & P1[x,y,z] holds z in F3() and A2: for x, y, z1, z2 being set st x in F1() & y in F2() & P1[x,y,z1] & P1[x,y,z2] holds z1 = z2 proof defpred S1[ set , set ] means for x1, y1 being set st \$1 = [x1,y1] holds P1[x1,y1,\$2]; A3: for x, z being set st x in [:F1(),F2():] & S1[x,z] holds z in F3() proof let x, z be set ; ::_thesis: ( x in [:F1(),F2():] & S1[x,z] implies z in F3() ) assume x in [:F1(),F2():] ; ::_thesis: ( not S1[x,z] or z in F3() ) then A4: ex x1, y1 being set st ( x1 in F1() & y1 in F2() & x = [x1,y1] ) by ZFMISC_1:def_2; assume for x1, y1 being set st x = [x1,y1] holds P1[x1,y1,z] ; ::_thesis: z in F3() hence z in F3() by A1, A4; ::_thesis: verum end; A5: for x, z1, z2 being set st x in [:F1(),F2():] & S1[x,z1] & S1[x,z2] holds z1 = z2 proof let x, z1, z2 be set ; ::_thesis: ( x in [:F1(),F2():] & S1[x,z1] & S1[x,z2] implies z1 = z2 ) assume that A6: x in [:F1(),F2():] and A7: ( ( for x1, y1 being set st x = [x1,y1] holds P1[x1,y1,z1] ) & ( for x1, y1 being set st x = [x1,y1] holds P1[x1,y1,z2] ) ) ; ::_thesis: z1 = z2 consider x1, y1 being set such that A8: ( x1 in F1() & y1 in F2() ) and A9: x = [x1,y1] by A6, ZFMISC_1:def_2; ( P1[x1,y1,z1] & P1[x1,y1,z2] ) by A7, A9; hence z1 = z2 by A2, A8; ::_thesis: verum end; consider f being PartFunc of [:F1(),F2():],F3() such that A10: for x being set holds ( x in dom f iff ( x in [:F1(),F2():] & ex z being set st S1[x,z] ) ) and A11: for x being set st x in dom f holds S1[x,f . x] from PARTFUN1:sch_2(A3, A5); take f ; ::_thesis: ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) ) & ( for x, y being set st [x,y] in dom f holds P1[x,y,f . (x,y)] ) ) thus for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) ::_thesis: for x, y being set st [x,y] in dom f holds P1[x,y,f . (x,y)] proof let x, y be set ; ::_thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) thus ( [x,y] in dom f implies ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) ::_thesis: ( x in F1() & y in F2() & ex z being set st P1[x,y,z] implies [x,y] in dom f ) proof assume A12: [x,y] in dom f ; ::_thesis: ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) hence ( x in F1() & y in F2() ) by ZFMISC_1:87; ::_thesis: ex z being set st P1[x,y,z] consider z being set such that A13: for x1, y1 being set st [x,y] = [x1,y1] holds P1[x1,y1,z] by A10, A12; take z ; ::_thesis: P1[x,y,z] thus P1[x,y,z] by A13; ::_thesis: verum end; assume ( x in F1() & y in F2() ) ; ::_thesis: ( for z being set holds P1[x,y,z] or [x,y] in dom f ) then A14: [x,y] in [:F1(),F2():] by ZFMISC_1:def_2; given z being set such that A15: P1[x,y,z] ; ::_thesis: [x,y] in dom f now__::_thesis:_ex_z_being_set_st_ for_x1,_y1_being_set_st_[x,y]_=_[x1,y1]_holds_ P1[x1,y1,z] take z = z; ::_thesis: for x1, y1 being set st [x,y] = [x1,y1] holds P1[x1,y1,z] let x1, y1 be set ; ::_thesis: ( [x,y] = [x1,y1] implies P1[x1,y1,z] ) assume A16: [x,y] = [x1,y1] ; ::_thesis: P1[x1,y1,z] then x = x1 by XTUPLE_0:1; hence P1[x1,y1,z] by A15, A16, XTUPLE_0:1; ::_thesis: verum end; hence [x,y] in dom f by A10, A14; ::_thesis: verum end; thus for x, y being set st [x,y] in dom f holds P1[x,y,f . (x,y)] by A11; ::_thesis: verum end; scheme :: BINOP_1:sch 6 LambdaR2{ F1() -> set , F2() -> set , F3() -> set , F4( set , set ) -> set , P1[ set , set ] } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) provided A1: for x, y being set st P1[x,y] holds F4(x,y) in F3() proof defpred S1[ set , set , set ] means ( P1[\$1,\$2] & \$3 = F4(\$1,\$2) ); A2: for x, y, z1, z2 being set st x in F1() & y in F2() & S1[x,y,z1] & S1[x,y,z2] holds z1 = z2 ; A3: for x, y, z being set st x in F1() & y in F2() & S1[x,y,z] holds z in F3() by A1; consider f being PartFunc of [:F1(),F2():],F3() such that A4: for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st S1[x,y,z] ) ) and A5: for x, y being set st [x,y] in dom f holds S1[x,y,f . (x,y)] from BINOP_1:sch_5(A3, A2); take f ; ::_thesis: ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) thus for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ::_thesis: for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) proof let x, y be set ; ::_thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) thus ( [x,y] in dom f implies ( x in F1() & y in F2() & P1[x,y] ) ) ::_thesis: ( x in F1() & y in F2() & P1[x,y] implies [x,y] in dom f ) proof assume A6: [x,y] in dom f ; ::_thesis: ( x in F1() & y in F2() & P1[x,y] ) then ex z being set st ( P1[x,y] & z = F4(x,y) ) by A4; hence ( x in F1() & y in F2() & P1[x,y] ) by A4, A6; ::_thesis: verum end; assume that A7: ( x in F1() & y in F2() ) and A8: P1[x,y] ; ::_thesis: [x,y] in dom f ex z being set st ( P1[x,y] & z = F4(x,y) ) by A8; hence [x,y] in dom f by A4, A7; ::_thesis: verum end; thus for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) by A5; ::_thesis: verum end; scheme :: BINOP_1:sch 7 PartLambda2{ F1() -> set , F2() -> set , F3() -> set , F4( set , set ) -> set , P1[ set , set ] } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) provided A1: for x, y being set st x in F1() & y in F2() & P1[x,y] holds F4(x,y) in F3() proof defpred S1[ set , set ] means ( \$1 in F1() & \$2 in F2() & P1[\$1,\$2] ); A2: for x, y being set st S1[x,y] holds F4(x,y) in F3() by A1; consider f being PartFunc of [:F1(),F2():],F3() such that A3: ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & S1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) from BINOP_1:sch_6(A2); take f ; ::_thesis: ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) thus ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) by A3; ::_thesis: verum end; scheme :: BINOP_1:sch 8 Sch8{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4( set , set ) -> set , P1[ set , set ] } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for x being Element of F1() for y being Element of F2() holds ( [x,y] in dom f iff P1[x,y] ) ) & ( for x being Element of F1() for y being Element of F2() st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) provided A1: for x being Element of F1() for y being Element of F2() st P1[x,y] holds F4(x,y) in F3() proof A2: for x, y being set st x in F1() & y in F2() & P1[x,y] holds F4(x,y) in F3() by A1; consider f being PartFunc of [:F1(),F2():],F3() such that A3: ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) from BINOP_1:sch_7(A2); take f ; ::_thesis: ( ( for x being Element of F1() for y being Element of F2() holds ( [x,y] in dom f iff P1[x,y] ) ) & ( for x being Element of F1() for y being Element of F2() st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) thus ( ( for x being Element of F1() for y being Element of F2() holds ( [x,y] in dom f iff P1[x,y] ) ) & ( for x being Element of F1() for y being Element of F2() st [x,y] in dom f holds f . (x,y) = F4(x,y) ) ) by A3; ::_thesis: verum end; definition let A be set ; let f be BinOp of A; let x, y be Element of A; :: original: . redefine funcf . (x,y) -> Element of A; coherence f . (x,y) is Element of A proof percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: f . (x,y) is Element of A then dom f = {} ; then f . (x,y) = {} by FUNCT_1:def_2; hence f . (x,y) is Element of A ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: f . (x,y) is Element of A then reconsider A = A as non empty set ; reconsider f = f as BinOp of A ; reconsider x = x, y = y as Element of A ; f . (x,y) is Element of A ; hence f . (x,y) is Element of A ; ::_thesis: verum end; end; end; end; definition let X, Y, Z be set ; let f1, f2 be Function of [:X,Y:],Z; :: original: = redefine predf1 = f2 means :: BINOP_1:def 21 for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y); compatibility ( f1 = f2 iff for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) ) by Th1; end; :: deftheorem defines = BINOP_1:def_21_:_ for X, Y, Z being set for f1, f2 being Function of [:X,Y:],Z holds ( f1 = f2 iff for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) );