:: PARTFUN2 semantic presentation begin theorem Th1: :: PARTFUN2:1 for D, C being non empty set for f, g being PartFunc of C,D st dom f = dom g & ( for c being Element of C st c in dom f holds f /. c = g /. c ) holds f = g proof let D, C be non empty set ; ::_thesis: for f, g being PartFunc of C,D st dom f = dom g & ( for c being Element of C st c in dom f holds f /. c = g /. c ) holds f = g let f, g be PartFunc of C,D; ::_thesis: ( dom f = dom g & ( for c being Element of C st c in dom f holds f /. c = g /. c ) implies f = g ) assume that A1: dom f = dom g and A2: for c being Element of C st c in dom f holds f /. c = g /. c ; ::_thesis: f = g now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in dom f implies f . x = g . x ) assume A3: x in dom f ; ::_thesis: f . x = g . x then reconsider y = x as Element of C ; f /. y = g /. y by A2, A3; then f . y = g /. y by A3, PARTFUN1:def_6; hence f . x = g . x by A1, A3, PARTFUN1:def_6; ::_thesis: verum end; hence f = g by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th2: :: PARTFUN2:2 for y being set for D, C being non empty set for f being PartFunc of C,D holds ( y in rng f iff ex c being Element of C st ( c in dom f & y = f /. c ) ) proof let y be set ; ::_thesis: for D, C being non empty set for f being PartFunc of C,D holds ( y in rng f iff ex c being Element of C st ( c in dom f & y = f /. c ) ) let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds ( y in rng f iff ex c being Element of C st ( c in dom f & y = f /. c ) ) let f be PartFunc of C,D; ::_thesis: ( y in rng f iff ex c being Element of C st ( c in dom f & y = f /. c ) ) thus ( y in rng f implies ex c being Element of C st ( c in dom f & y = f /. c ) ) ::_thesis: ( ex c being Element of C st ( c in dom f & y = f /. c ) implies y in rng f ) proof assume y in rng f ; ::_thesis: ex c being Element of C st ( c in dom f & y = f /. c ) then consider x being set such that A1: x in dom f and A2: y = f . x by FUNCT_1:def_3; reconsider x = x as Element of C by A1; take x ; ::_thesis: ( x in dom f & y = f /. x ) thus ( x in dom f & y = f /. x ) by A1, A2, PARTFUN1:def_6; ::_thesis: verum end; given c being Element of C such that A3: c in dom f and A4: y = f /. c ; ::_thesis: y in rng f f . c in rng f by A3, FUNCT_1:def_3; hence y in rng f by A3, A4, PARTFUN1:def_6; ::_thesis: verum end; theorem Th3: :: PARTFUN2:3 for D, E, C being non empty set for f being PartFunc of C,D for s being PartFunc of D,E for h being PartFunc of C,E holds ( h = s * f iff ( ( for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ) ) ) proof let D, E, C be non empty set ; ::_thesis: for f being PartFunc of C,D for s being PartFunc of D,E for h being PartFunc of C,E holds ( h = s * f iff ( ( for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ) ) ) let f be PartFunc of C,D; ::_thesis: for s being PartFunc of D,E for h being PartFunc of C,E holds ( h = s * f iff ( ( for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ) ) ) let s be PartFunc of D,E; ::_thesis: for h being PartFunc of C,E holds ( h = s * f iff ( ( for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ) ) ) let h be PartFunc of C,E; ::_thesis: ( h = s * f iff ( ( for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ) ) ) thus ( h = s * f implies ( ( for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ) ) ) ::_thesis: ( ( for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ) implies h = s * f ) proof assume A1: h = s * f ; ::_thesis: ( ( for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ) ) A2: now__::_thesis:_for_c_being_Element_of_C_holds_ (_(_c_in_dom_h_implies_(_c_in_dom_f_&_f_/._c_in_dom_s_)_)_&_(_c_in_dom_f_&_f_/._c_in_dom_s_implies_c_in_dom_h_)_) let c be Element of C; ::_thesis: ( ( c in dom h implies ( c in dom f & f /. c in dom s ) ) & ( c in dom f & f /. c in dom s implies c in dom h ) ) thus ( c in dom h implies ( c in dom f & f /. c in dom s ) ) ::_thesis: ( c in dom f & f /. c in dom s implies c in dom h ) proof assume c in dom h ; ::_thesis: ( c in dom f & f /. c in dom s ) then ( c in dom f & f . c in dom s ) by A1, FUNCT_1:11; hence ( c in dom f & f /. c in dom s ) by PARTFUN1:def_6; ::_thesis: verum end; assume that A3: c in dom f and A4: f /. c in dom s ; ::_thesis: c in dom h f . c in dom s by A3, A4, PARTFUN1:def_6; hence c in dom h by A1, A3, FUNCT_1:11; ::_thesis: verum end; hence for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) ; ::_thesis: for c being Element of C st c in dom h holds h /. c = s /. (f /. c) let c be Element of C; ::_thesis: ( c in dom h implies h /. c = s /. (f /. c) ) assume A5: c in dom h ; ::_thesis: h /. c = s /. (f /. c) then h . c = s . (f . c) by A1, FUNCT_1:12; then A6: h /. c = s . (f . c) by A5, PARTFUN1:def_6; c in dom f by A2, A5; then A7: h /. c = s . (f /. c) by A6, PARTFUN1:def_6; f /. c in dom s by A2, A5; hence h /. c = s /. (f /. c) by A7, PARTFUN1:def_6; ::_thesis: verum end; assume that A8: for c being Element of C holds ( c in dom h iff ( c in dom f & f /. c in dom s ) ) and A9: for c being Element of C st c in dom h holds h /. c = s /. (f /. c) ; ::_thesis: h = s * f A10: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_h_implies_(_x_in_dom_f_&_f_._x_in_dom_s_)_)_&_(_x_in_dom_f_&_f_._x_in_dom_s_implies_x_in_dom_h_)_) let x be set ; ::_thesis: ( ( x in dom h implies ( x in dom f & f . x in dom s ) ) & ( x in dom f & f . x in dom s implies x in dom h ) ) thus ( x in dom h implies ( x in dom f & f . x in dom s ) ) ::_thesis: ( x in dom f & f . x in dom s implies x in dom h ) proof assume A11: x in dom h ; ::_thesis: ( x in dom f & f . x in dom s ) then reconsider y = x as Element of C ; ( y in dom f & f /. y in dom s ) by A8, A11; hence ( x in dom f & f . x in dom s ) by PARTFUN1:def_6; ::_thesis: verum end; thus ( x in dom f & f . x in dom s implies x in dom h ) ::_thesis: verum proof assume that A12: x in dom f and A13: f . x in dom s ; ::_thesis: x in dom h reconsider y = x as Element of C by A12; f /. y in dom s by A12, A13, PARTFUN1:def_6; hence x in dom h by A8, A12; ::_thesis: verum end; end; now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_ h_._x_=_s_._(f_._x) let x be set ; ::_thesis: ( x in dom h implies h . x = s . (f . x) ) assume A14: x in dom h ; ::_thesis: h . x = s . (f . x) then reconsider y = x as Element of C ; h /. y = s /. (f /. y) by A9, A14; then A15: h . y = s /. (f /. y) by A14, PARTFUN1:def_6; f /. y in dom s by A8, A14; then A16: h . x = s . (f /. y) by A15, PARTFUN1:def_6; y in dom f by A8, A14; hence h . x = s . (f . x) by A16, PARTFUN1:def_6; ::_thesis: verum end; hence h = s * f by A10, FUNCT_1:10; ::_thesis: verum end; theorem Th4: :: PARTFUN2:4 for C, D, E being non empty set for c being Element of C for f being PartFunc of C,D for s being PartFunc of D,E st c in dom f & f /. c in dom s holds (s * f) /. c = s /. (f /. c) proof let C, D, E be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,D for s being PartFunc of D,E st c in dom f & f /. c in dom s holds (s * f) /. c = s /. (f /. c) let c be Element of C; ::_thesis: for f being PartFunc of C,D for s being PartFunc of D,E st c in dom f & f /. c in dom s holds (s * f) /. c = s /. (f /. c) let f be PartFunc of C,D; ::_thesis: for s being PartFunc of D,E st c in dom f & f /. c in dom s holds (s * f) /. c = s /. (f /. c) let s be PartFunc of D,E; ::_thesis: ( c in dom f & f /. c in dom s implies (s * f) /. c = s /. (f /. c) ) assume ( c in dom f & f /. c in dom s ) ; ::_thesis: (s * f) /. c = s /. (f /. c) then c in dom (s * f) by Th3; hence (s * f) /. c = s /. (f /. c) by Th3; ::_thesis: verum end; theorem :: PARTFUN2:5 for C, D, E being non empty set for c being Element of C for f being PartFunc of C,D for s being PartFunc of D,E st rng f c= dom s & c in dom f holds (s * f) /. c = s /. (f /. c) proof let C, D, E be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,D for s being PartFunc of D,E st rng f c= dom s & c in dom f holds (s * f) /. c = s /. (f /. c) let c be Element of C; ::_thesis: for f being PartFunc of C,D for s being PartFunc of D,E st rng f c= dom s & c in dom f holds (s * f) /. c = s /. (f /. c) let f be PartFunc of C,D; ::_thesis: for s being PartFunc of D,E st rng f c= dom s & c in dom f holds (s * f) /. c = s /. (f /. c) let s be PartFunc of D,E; ::_thesis: ( rng f c= dom s & c in dom f implies (s * f) /. c = s /. (f /. c) ) assume that A1: rng f c= dom s and A2: c in dom f ; ::_thesis: (s * f) /. c = s /. (f /. c) f /. c in rng f by A2, Th2; hence (s * f) /. c = s /. (f /. c) by A1, A2, Th4; ::_thesis: verum end; definition let D be non empty set ; let SD be Subset of D; :: original: id redefine func id SD -> PartFunc of D,D; coherence id SD is PartFunc of D,D proof ( dom (id SD) = SD & rng (id SD) = SD ) by RELAT_1:45; hence id SD is PartFunc of D,D by RELSET_1:4; ::_thesis: verum end; end; theorem Th6: :: PARTFUN2:6 for D being non empty set for SD being Subset of D for F being PartFunc of D,D holds ( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds F /. d = d ) ) ) proof let D be non empty set ; ::_thesis: for SD being Subset of D for F being PartFunc of D,D holds ( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds F /. d = d ) ) ) let SD be Subset of D; ::_thesis: for F being PartFunc of D,D holds ( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds F /. d = d ) ) ) let F be PartFunc of D,D; ::_thesis: ( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds F /. d = d ) ) ) thus ( F = id SD implies ( dom F = SD & ( for d being Element of D st d in SD holds F /. d = d ) ) ) ::_thesis: ( dom F = SD & ( for d being Element of D st d in SD holds F /. d = d ) implies F = id SD ) proof assume A1: F = id SD ; ::_thesis: ( dom F = SD & ( for d being Element of D st d in SD holds F /. d = d ) ) hence A2: dom F = SD by RELAT_1:45; ::_thesis: for d being Element of D st d in SD holds F /. d = d let d be Element of D; ::_thesis: ( d in SD implies F /. d = d ) assume A3: d in SD ; ::_thesis: F /. d = d then F . d = d by A1, FUNCT_1:18; hence F /. d = d by A2, A3, PARTFUN1:def_6; ::_thesis: verum end; assume that A4: dom F = SD and A5: for d being Element of D st d in SD holds F /. d = d ; ::_thesis: F = id SD now__::_thesis:_for_x_being_set_st_x_in_SD_holds_ F_._x_=_x let x be set ; ::_thesis: ( x in SD implies F . x = x ) assume A6: x in SD ; ::_thesis: F . x = x then reconsider x1 = x as Element of D ; F /. x1 = x1 by A5, A6; hence F . x = x by A4, A6, PARTFUN1:def_6; ::_thesis: verum end; hence F = id SD by A4, FUNCT_1:17; ::_thesis: verum end; theorem :: PARTFUN2:7 for D being non empty set for SD being Subset of D for d being Element of D for F being PartFunc of D,D st d in (dom F) /\ SD holds F /. d = (F * (id SD)) /. d proof let D be non empty set ; ::_thesis: for SD being Subset of D for d being Element of D for F being PartFunc of D,D st d in (dom F) /\ SD holds F /. d = (F * (id SD)) /. d let SD be Subset of D; ::_thesis: for d being Element of D for F being PartFunc of D,D st d in (dom F) /\ SD holds F /. d = (F * (id SD)) /. d let d be Element of D; ::_thesis: for F being PartFunc of D,D st d in (dom F) /\ SD holds F /. d = (F * (id SD)) /. d let F be PartFunc of D,D; ::_thesis: ( d in (dom F) /\ SD implies F /. d = (F * (id SD)) /. d ) assume A1: d in (dom F) /\ SD ; ::_thesis: F /. d = (F * (id SD)) /. d then A2: d in dom F by XBOOLE_0:def_4; F . d = (F * (id SD)) . d by A1, FUNCT_1:20; then A3: F /. d = (F * (id SD)) . d by A2, PARTFUN1:def_6; A4: d in SD by A1, XBOOLE_0:def_4; then A5: d in dom (id SD) by RELAT_1:45; (id SD) /. d in dom F by A2, A4, Th6; then d in dom (F * (id SD)) by A5, Th3; hence F /. d = (F * (id SD)) /. d by A3, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:8 for D being non empty set for SD being Subset of D for d being Element of D for F being PartFunc of D,D holds ( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) ) proof let D be non empty set ; ::_thesis: for SD being Subset of D for d being Element of D for F being PartFunc of D,D holds ( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) ) let SD be Subset of D; ::_thesis: for d being Element of D for F being PartFunc of D,D holds ( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) ) let d be Element of D; ::_thesis: for F being PartFunc of D,D holds ( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) ) let F be PartFunc of D,D; ::_thesis: ( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) ) thus ( d in dom ((id SD) * F) implies ( d in dom F & F /. d in SD ) ) ::_thesis: ( d in dom F & F /. d in SD implies d in dom ((id SD) * F) ) proof assume A1: d in dom ((id SD) * F) ; ::_thesis: ( d in dom F & F /. d in SD ) then F /. d in dom (id SD) by Th3; hence ( d in dom F & F /. d in SD ) by A1, Th3, RELAT_1:45; ::_thesis: verum end; assume that A2: d in dom F and A3: F /. d in SD ; ::_thesis: d in dom ((id SD) * F) F /. d in dom (id SD) by A3, RELAT_1:45; hence d in dom ((id SD) * F) by A2, Th3; ::_thesis: verum end; theorem :: PARTFUN2:9 for D, C being non empty set for f being PartFunc of C,D st ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds c1 = c2 ) holds f is one-to-one proof let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D st ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds c1 = c2 ) holds f is one-to-one let f be PartFunc of C,D; ::_thesis: ( ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds c1 = c2 ) implies f is one-to-one ) assume A1: for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds c1 = c2 ; ::_thesis: f is one-to-one now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_f_&_f_._x_=_f_._y_holds_ x_=_y let x, y be set ; ::_thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y ) assume that A2: x in dom f and A3: y in dom f and A4: f . x = f . y ; ::_thesis: x = y reconsider y1 = y as Element of C by A3; reconsider x1 = x as Element of C by A2; f /. x1 = f . y1 by A2, A4, PARTFUN1:def_6; then f /. x1 = f /. y1 by A3, PARTFUN1:def_6; hence x = y by A1, A2, A3; ::_thesis: verum end; hence f is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; theorem :: PARTFUN2:10 for x, y being set for C, D being non empty set for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds x = y proof let x, y be set ; ::_thesis: for C, D being non empty set for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds x = y let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds x = y let f be PartFunc of C,D; ::_thesis: ( f is one-to-one & x in dom f & y in dom f & f /. x = f /. y implies x = y ) assume that A1: f is one-to-one and A2: x in dom f and A3: y in dom f ; ::_thesis: ( not f /. x = f /. y or x = y ) assume f /. x = f /. y ; ::_thesis: x = y then f . x = f /. y by A2, PARTFUN1:def_6 .= f . y by A3, PARTFUN1:def_6 ; hence x = y by A1, A2, A3, FUNCT_1:def_4; ::_thesis: verum end; definition let X, Y be set ; let f be one-to-one PartFunc of X,Y; :: original: " redefine funcf " -> PartFunc of Y,X; coherence f " is PartFunc of Y,X by PARTFUN1:9; end; theorem Th11: :: PARTFUN2:11 for C, D being non empty set for f being one-to-one PartFunc of C,D for g being PartFunc of D,C holds ( g = f " iff ( dom g = rng f & ( for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) proof let C, D be non empty set ; ::_thesis: for f being one-to-one PartFunc of C,D for g being PartFunc of D,C holds ( g = f " iff ( dom g = rng f & ( for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) let f be one-to-one PartFunc of C,D; ::_thesis: for g being PartFunc of D,C holds ( g = f " iff ( dom g = rng f & ( for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) let g be PartFunc of D,C; ::_thesis: ( g = f " iff ( dom g = rng f & ( for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) thus ( g = f " implies ( dom g = rng f & ( for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) ::_thesis: ( dom g = rng f & ( for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) implies g = f " ) proof assume A1: g = f " ; ::_thesis: ( dom g = rng f & ( for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) hence dom g = rng f by FUNCT_1:32; ::_thesis: for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) let d be Element of D; ::_thesis: for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) let c be Element of C; ::_thesis: ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) A2: dom g = rng f by A1, FUNCT_1:32; thus ( d in rng f & c = g /. d implies ( c in dom f & d = f /. c ) ) ::_thesis: ( c in dom f & d = f /. c implies ( d in rng f & c = g /. d ) ) proof assume that A3: d in rng f and A4: c = g /. d ; ::_thesis: ( c in dom f & d = f /. c ) c = g . d by A2, A3, A4, PARTFUN1:def_6; then ( c in dom f & d = f . c ) by A1, A3, FUNCT_1:32; hence ( c in dom f & d = f /. c ) by PARTFUN1:def_6; ::_thesis: verum end; assume that A5: c in dom f and A6: d = f /. c ; ::_thesis: ( d in rng f & c = g /. d ) d = f . c by A5, A6, PARTFUN1:def_6; then ( d in rng f & c = g . d ) by A1, A5, FUNCT_1:32; hence ( d in rng f & c = g /. d ) by A2, PARTFUN1:def_6; ::_thesis: verum end; assume that A7: dom g = rng f and A8: for d being Element of D for c being Element of C holds ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) and A9: g <> f " ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( dom (f ") <> dom g or ex d being Element of D st ( d in dom (f ") & (f ") /. d <> g /. d ) ) by A9, Th1; suppose dom (f ") <> dom g ; ::_thesis: contradiction hence contradiction by A7, FUNCT_1:33; ::_thesis: verum end; suppose ex d being Element of D st ( d in dom (f ") & (f ") /. d <> g /. d ) ; ::_thesis: contradiction then consider d being Element of D such that A10: d in dom (f ") and A11: (f ") /. d <> g /. d ; (f ") /. d in rng (f ") by A10, Th2; then A12: (f ") /. d in dom f by FUNCT_1:33; d in rng f by A10, FUNCT_1:33; then d = f . ((f ") . d) by FUNCT_1:35; then d = f . ((f ") /. d) by A10, PARTFUN1:def_6; then d = f /. ((f ") /. d) by A12, PARTFUN1:def_6; hence contradiction by A8, A11, A12; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem :: PARTFUN2:12 for C, D being non empty set for c being Element of C for f being one-to-one PartFunc of C,D st c in dom f holds ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c ) proof let C, D be non empty set ; ::_thesis: for c being Element of C for f being one-to-one PartFunc of C,D st c in dom f holds ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c ) let c be Element of C; ::_thesis: for f being one-to-one PartFunc of C,D st c in dom f holds ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c ) let f be one-to-one PartFunc of C,D; ::_thesis: ( c in dom f implies ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c ) ) assume A1: c in dom f ; ::_thesis: ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c ) hence A2: c = (f ") /. (f /. c) by Th11; ::_thesis: c = ((f ") * f) /. c f " = f " ; then f /. c in rng f by A1, Th11; then f /. c in dom (f ") by FUNCT_1:33; hence c = ((f ") * f) /. c by A1, A2, Th4; ::_thesis: verum end; theorem :: PARTFUN2:13 for C, D being non empty set for d being Element of D for f being one-to-one PartFunc of C,D st d in rng f holds ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) proof let C, D be non empty set ; ::_thesis: for d being Element of D for f being one-to-one PartFunc of C,D st d in rng f holds ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) let d be Element of D; ::_thesis: for f being one-to-one PartFunc of C,D st d in rng f holds ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) let f be one-to-one PartFunc of C,D; ::_thesis: ( d in rng f implies ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) ) assume A1: d in rng f ; ::_thesis: ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) then ( d = (f * (f ")) . d & d in dom (f * (f ")) ) by FUNCT_1:35, FUNCT_1:37; hence ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) by A1, Th11, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:14 for C, D being non empty set for f being PartFunc of C,D for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C for d being Element of D st c in dom f & d in dom t holds ( f /. c = d iff t /. d = c ) ) holds t = f " proof let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C for d being Element of D st c in dom f & d in dom t holds ( f /. c = d iff t /. d = c ) ) holds t = f " let f be PartFunc of C,D; ::_thesis: for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C for d being Element of D st c in dom f & d in dom t holds ( f /. c = d iff t /. d = c ) ) holds t = f " let t be PartFunc of D,C; ::_thesis: ( f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C for d being Element of D st c in dom f & d in dom t holds ( f /. c = d iff t /. d = c ) ) implies t = f " ) assume that A1: ( f is one-to-one & dom f = rng t & rng f = dom t ) and A2: for c being Element of C for d being Element of D st c in dom f & d in dom t holds ( f /. c = d iff t /. d = c ) ; ::_thesis: t = f " now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_t_holds_ (_(_f_._x_=_y_implies_t_._y_=_x_)_&_(_t_._y_=_x_implies_f_._x_=_y_)_) let x, y be set ; ::_thesis: ( x in dom f & y in dom t implies ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) ) ) assume that A3: x in dom f and A4: y in dom t ; ::_thesis: ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) ) reconsider y1 = y as Element of D by A4; reconsider x1 = x as Element of C by A3; thus ( f . x = y implies t . y = x ) ::_thesis: ( t . y = x implies f . x = y ) proof assume f . x = y ; ::_thesis: t . y = x then f /. x1 = y1 by A3, PARTFUN1:def_6; then t /. y1 = x1 by A2, A3, A4; hence t . y = x by A4, PARTFUN1:def_6; ::_thesis: verum end; assume t . y = x ; ::_thesis: f . x = y then t /. y1 = x1 by A4, PARTFUN1:def_6; then f /. x1 = y1 by A2, A3, A4; hence f . x = y by A3, PARTFUN1:def_6; ::_thesis: verum end; hence t = f " by A1, FUNCT_1:38; ::_thesis: verum end; theorem Th15: :: PARTFUN2:15 for X being set for D, C being non empty set for g, f being PartFunc of C,D holds ( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) proof let X be set ; ::_thesis: for D, C being non empty set for g, f being PartFunc of C,D holds ( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) let D, C be non empty set ; ::_thesis: for g, f being PartFunc of C,D holds ( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) let g, f be PartFunc of C,D; ::_thesis: ( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) thus ( g = f | X implies ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) ::_thesis: ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds g /. c = f /. c ) implies g = f | X ) proof assume A1: g = f | X ; ::_thesis: ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) hence dom g = (dom f) /\ X by RELAT_1:61; ::_thesis: for c being Element of C st c in dom g holds g /. c = f /. c let c be Element of C; ::_thesis: ( c in dom g implies g /. c = f /. c ) assume A2: c in dom g ; ::_thesis: g /. c = f /. c then g . c = f . c by A1, FUNCT_1:47; then A3: g /. c = f . c by A2, PARTFUN1:def_6; dom g = (dom f) /\ X by A1, RELAT_1:61; then c in dom f by A2, XBOOLE_0:def_4; hence g /. c = f /. c by A3, PARTFUN1:def_6; ::_thesis: verum end; assume that A4: dom g = (dom f) /\ X and A5: for c being Element of C st c in dom g holds g /. c = f /. c ; ::_thesis: g = f | X now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_ g_._x_=_f_._x let x be set ; ::_thesis: ( x in dom g implies g . x = f . x ) assume A6: x in dom g ; ::_thesis: g . x = f . x then reconsider y = x as Element of C ; g /. y = f /. y by A5, A6; then A7: g . y = f /. y by A6, PARTFUN1:def_6; x in dom f by A4, A6, XBOOLE_0:def_4; hence g . x = f . x by A7, PARTFUN1:def_6; ::_thesis: verum end; hence g = f | X by A4, FUNCT_1:46; ::_thesis: verum end; theorem Th16: :: PARTFUN2:16 for X being set for C, D being non empty set for c being Element of C for f being PartFunc of C,D st c in (dom f) /\ X holds (f | X) /. c = f /. c proof let X be set ; ::_thesis: for C, D being non empty set for c being Element of C for f being PartFunc of C,D st c in (dom f) /\ X holds (f | X) /. c = f /. c let C, D be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,D st c in (dom f) /\ X holds (f | X) /. c = f /. c let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in (dom f) /\ X holds (f | X) /. c = f /. c let f be PartFunc of C,D; ::_thesis: ( c in (dom f) /\ X implies (f | X) /. c = f /. c ) assume c in (dom f) /\ X ; ::_thesis: (f | X) /. c = f /. c then c in dom (f | X) by RELAT_1:61; hence (f | X) /. c = f /. c by Th15; ::_thesis: verum end; theorem :: PARTFUN2:17 for X being set for C, D being non empty set for c being Element of C for f being PartFunc of C,D st c in dom f & c in X holds (f | X) /. c = f /. c proof let X be set ; ::_thesis: for C, D being non empty set for c being Element of C for f being PartFunc of C,D st c in dom f & c in X holds (f | X) /. c = f /. c let C, D be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,D st c in dom f & c in X holds (f | X) /. c = f /. c let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in dom f & c in X holds (f | X) /. c = f /. c let f be PartFunc of C,D; ::_thesis: ( c in dom f & c in X implies (f | X) /. c = f /. c ) assume ( c in dom f & c in X ) ; ::_thesis: (f | X) /. c = f /. c then c in (dom f) /\ X by XBOOLE_0:def_4; hence (f | X) /. c = f /. c by Th16; ::_thesis: verum end; theorem :: PARTFUN2:18 for X being set for C, D being non empty set for c being Element of C for f being PartFunc of C,D st c in dom f & c in X holds f /. c in rng (f | X) proof let X be set ; ::_thesis: for C, D being non empty set for c being Element of C for f being PartFunc of C,D st c in dom f & c in X holds f /. c in rng (f | X) let C, D be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,D st c in dom f & c in X holds f /. c in rng (f | X) let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in dom f & c in X holds f /. c in rng (f | X) let f be PartFunc of C,D; ::_thesis: ( c in dom f & c in X implies f /. c in rng (f | X) ) assume that A1: c in dom f and A2: c in X ; ::_thesis: f /. c in rng (f | X) f . c in rng (f | X) by A1, A2, FUNCT_1:50; hence f /. c in rng (f | X) by A1, PARTFUN1:def_6; ::_thesis: verum end; definition let C, D be non empty set ; let X be set ; let f be PartFunc of C,D; :: original: |` redefine funcX |` f -> PartFunc of C,D; coherence X |` f is PartFunc of C,D by PARTFUN1:13; end; theorem Th19: :: PARTFUN2:19 for X being set for D, C being non empty set for g, f being PartFunc of C,D holds ( g = X |` f iff ( ( for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) proof let X be set ; ::_thesis: for D, C being non empty set for g, f being PartFunc of C,D holds ( g = X |` f iff ( ( for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) let D, C be non empty set ; ::_thesis: for g, f being PartFunc of C,D holds ( g = X |` f iff ( ( for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) let g, f be PartFunc of C,D; ::_thesis: ( g = X |` f iff ( ( for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) thus ( g = X |` f implies ( ( for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) ) ::_thesis: ( ( for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds g /. c = f /. c ) implies g = X |` f ) proof assume A1: g = X |` f ; ::_thesis: ( ( for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds g /. c = f /. c ) ) now__::_thesis:_for_c_being_Element_of_C_holds_ (_(_c_in_dom_g_implies_(_c_in_dom_f_&_f_/._c_in_X_)_)_&_(_c_in_dom_f_&_f_/._c_in_X_implies_c_in_dom_g_)_) let c be Element of C; ::_thesis: ( ( c in dom g implies ( c in dom f & f /. c in X ) ) & ( c in dom f & f /. c in X implies c in dom g ) ) thus ( c in dom g implies ( c in dom f & f /. c in X ) ) ::_thesis: ( c in dom f & f /. c in X implies c in dom g ) proof assume c in dom g ; ::_thesis: ( c in dom f & f /. c in X ) then ( c in dom f & f . c in X ) by A1, FUNCT_1:54; hence ( c in dom f & f /. c in X ) by PARTFUN1:def_6; ::_thesis: verum end; assume that A2: c in dom f and A3: f /. c in X ; ::_thesis: c in dom g f . c in X by A2, A3, PARTFUN1:def_6; hence c in dom g by A1, A2, FUNCT_1:54; ::_thesis: verum end; hence for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) ; ::_thesis: for c being Element of C st c in dom g holds g /. c = f /. c let c be Element of C; ::_thesis: ( c in dom g implies g /. c = f /. c ) assume A4: c in dom g ; ::_thesis: g /. c = f /. c then g . c = f . c by A1, FUNCT_1:55; then A5: g /. c = f . c by A4, PARTFUN1:def_6; c in dom f by A1, A4, FUNCT_1:54; hence g /. c = f /. c by A5, PARTFUN1:def_6; ::_thesis: verum end; assume that A6: for c being Element of C holds ( c in dom g iff ( c in dom f & f /. c in X ) ) and A7: for c being Element of C st c in dom g holds g /. c = f /. c ; ::_thesis: g = X |` f A8: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_g_implies_(_x_in_dom_f_&_f_._x_in_X_)_)_&_(_x_in_dom_f_&_f_._x_in_X_implies_x_in_dom_g_)_) let x be set ; ::_thesis: ( ( x in dom g implies ( x in dom f & f . x in X ) ) & ( x in dom f & f . x in X implies x in dom g ) ) thus ( x in dom g implies ( x in dom f & f . x in X ) ) ::_thesis: ( x in dom f & f . x in X implies x in dom g ) proof assume A9: x in dom g ; ::_thesis: ( x in dom f & f . x in X ) then reconsider x1 = x as Element of C ; ( x1 in dom f & f /. x1 in X ) by A6, A9; hence ( x in dom f & f . x in X ) by PARTFUN1:def_6; ::_thesis: verum end; assume that A10: x in dom f and A11: f . x in X ; ::_thesis: x in dom g reconsider x1 = x as Element of C by A10; f /. x1 in X by A10, A11, PARTFUN1:def_6; hence x in dom g by A6, A10; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_ g_._x_=_f_._x let x be set ; ::_thesis: ( x in dom g implies g . x = f . x ) assume A12: x in dom g ; ::_thesis: g . x = f . x then reconsider x1 = x as Element of C ; g /. x1 = f /. x1 by A7, A12; then A13: g . x1 = f /. x1 by A12, PARTFUN1:def_6; x1 in dom f by A6, A12; hence g . x = f . x by A13, PARTFUN1:def_6; ::_thesis: verum end; hence g = X |` f by A8, FUNCT_1:53; ::_thesis: verum end; theorem :: PARTFUN2:20 for X being set for C, D being non empty set for c being Element of C for f being PartFunc of C,D holds ( c in dom (X |` f) iff ( c in dom f & f /. c in X ) ) by Th19; theorem :: PARTFUN2:21 for X being set for C, D being non empty set for c being Element of C for f being PartFunc of C,D st c in dom (X |` f) holds (X |` f) /. c = f /. c by Th19; theorem Th22: :: PARTFUN2:22 for X being set for D, C being non empty set for SD being Subset of D for f being PartFunc of C,D holds ( SD = f .: X iff for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) ) proof let X be set ; ::_thesis: for D, C being non empty set for SD being Subset of D for f being PartFunc of C,D holds ( SD = f .: X iff for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) ) let D, C be non empty set ; ::_thesis: for SD being Subset of D for f being PartFunc of C,D holds ( SD = f .: X iff for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) ) let SD be Subset of D; ::_thesis: for f being PartFunc of C,D holds ( SD = f .: X iff for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) ) let f be PartFunc of C,D; ::_thesis: ( SD = f .: X iff for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) ) thus ( SD = f .: X implies for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) ) ::_thesis: ( ( for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) ) implies SD = f .: X ) proof assume A1: SD = f .: X ; ::_thesis: for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) let d be Element of D; ::_thesis: ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) thus ( d in SD implies ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) ::_thesis: ( ex c being Element of C st ( c in dom f & c in X & d = f /. c ) implies d in SD ) proof assume d in SD ; ::_thesis: ex c being Element of C st ( c in dom f & c in X & d = f /. c ) then consider x being set such that A2: x in dom f and A3: x in X and A4: d = f . x by A1, FUNCT_1:def_6; reconsider x = x as Element of C by A2; take x ; ::_thesis: ( x in dom f & x in X & d = f /. x ) thus ( x in dom f & x in X ) by A2, A3; ::_thesis: d = f /. x thus d = f /. x by A2, A4, PARTFUN1:def_6; ::_thesis: verum end; given c being Element of C such that A5: c in dom f and A6: ( c in X & d = f /. c ) ; ::_thesis: d in SD f /. c = f . c by A5, PARTFUN1:def_6; hence d in SD by A1, A5, A6, FUNCT_1:def_6; ::_thesis: verum end; assume that A7: for d being Element of D holds ( d in SD iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) and A8: SD <> f .: X ; ::_thesis: contradiction consider x being set such that A9: ( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) ) by A8, TARSKI:1; now__::_thesis:_contradiction percases ( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) ) by A9; supposeA10: ( x in SD & not x in f .: X ) ; ::_thesis: contradiction then reconsider x = x as Element of D ; consider c being Element of C such that A11: c in dom f and A12: c in X and A13: x = f /. c by A7, A10; x = f . c by A11, A13, PARTFUN1:def_6; hence contradiction by A10, A11, A12, FUNCT_1:def_6; ::_thesis: verum end; supposeA14: ( x in f .: X & not x in SD ) ; ::_thesis: contradiction then consider y being set such that A15: y in dom f and A16: y in X and A17: x = f . y by FUNCT_1:def_6; reconsider y = y as Element of C by A15; x = f /. y by A15, A17, PARTFUN1:def_6; hence contradiction by A7, A14, A15, A16; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem :: PARTFUN2:23 for X being set for C, D being non empty set for d being Element of D for f being PartFunc of C,D holds ( d in f .: X iff ex c being Element of C st ( c in dom f & c in X & d = f /. c ) ) by Th22; theorem :: PARTFUN2:24 for C, D being non empty set for c being Element of C for f being PartFunc of C,D st c in dom f holds Im (f,c) = {(f /. c)} proof let C, D be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,D st c in dom f holds Im (f,c) = {(f /. c)} let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in dom f holds Im (f,c) = {(f /. c)} let f be PartFunc of C,D; ::_thesis: ( c in dom f implies Im (f,c) = {(f /. c)} ) assume A1: c in dom f ; ::_thesis: Im (f,c) = {(f /. c)} hence Im (f,c) = {(f . c)} by FUNCT_1:59 .= {(f /. c)} by A1, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: PARTFUN2:25 for C, D being non empty set for c1, c2 being Element of C for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds f .: {c1,c2} = {(f /. c1),(f /. c2)} proof let C, D be non empty set ; ::_thesis: for c1, c2 being Element of C for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds f .: {c1,c2} = {(f /. c1),(f /. c2)} let c1, c2 be Element of C; ::_thesis: for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds f .: {c1,c2} = {(f /. c1),(f /. c2)} let f be PartFunc of C,D; ::_thesis: ( c1 in dom f & c2 in dom f implies f .: {c1,c2} = {(f /. c1),(f /. c2)} ) assume that A1: c1 in dom f and A2: c2 in dom f ; ::_thesis: f .: {c1,c2} = {(f /. c1),(f /. c2)} thus f .: {c1,c2} = {(f . c1),(f . c2)} by A1, A2, FUNCT_1:60 .= {(f /. c1),(f . c2)} by A1, PARTFUN1:def_6 .= {(f /. c1),(f /. c2)} by A2, PARTFUN1:def_6 ; ::_thesis: verum end; theorem Th26: :: PARTFUN2:26 for X being set for D, C being non empty set for SC being Subset of C for f being PartFunc of C,D holds ( SC = f " X iff for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) ) proof let X be set ; ::_thesis: for D, C being non empty set for SC being Subset of C for f being PartFunc of C,D holds ( SC = f " X iff for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) ) let D, C be non empty set ; ::_thesis: for SC being Subset of C for f being PartFunc of C,D holds ( SC = f " X iff for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) ) let SC be Subset of C; ::_thesis: for f being PartFunc of C,D holds ( SC = f " X iff for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) ) let f be PartFunc of C,D; ::_thesis: ( SC = f " X iff for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) ) thus ( SC = f " X implies for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) ) ::_thesis: ( ( for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) ) implies SC = f " X ) proof assume A1: SC = f " X ; ::_thesis: for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) let c be Element of C; ::_thesis: ( c in SC iff ( c in dom f & f /. c in X ) ) thus ( c in SC implies ( c in dom f & f /. c in X ) ) ::_thesis: ( c in dom f & f /. c in X implies c in SC ) proof assume c in SC ; ::_thesis: ( c in dom f & f /. c in X ) then ( c in dom f & f . c in X ) by A1, FUNCT_1:def_7; hence ( c in dom f & f /. c in X ) by PARTFUN1:def_6; ::_thesis: verum end; assume that A2: c in dom f and A3: f /. c in X ; ::_thesis: c in SC f . c in X by A2, A3, PARTFUN1:def_6; hence c in SC by A1, A2, FUNCT_1:def_7; ::_thesis: verum end; assume A4: for c being Element of C holds ( c in SC iff ( c in dom f & f /. c in X ) ) ; ::_thesis: SC = f " X now__::_thesis:_for_x_being_set_holds_ (_(_x_in_SC_implies_(_x_in_dom_f_&_f_._x_in_X_)_)_&_(_x_in_dom_f_&_f_._x_in_X_implies_x_in_SC_)_) let x be set ; ::_thesis: ( ( x in SC implies ( x in dom f & f . x in X ) ) & ( x in dom f & f . x in X implies x in SC ) ) thus ( x in SC implies ( x in dom f & f . x in X ) ) ::_thesis: ( x in dom f & f . x in X implies x in SC ) proof assume A5: x in SC ; ::_thesis: ( x in dom f & f . x in X ) then reconsider x1 = x as Element of C ; ( x1 in dom f & f /. x1 in X ) by A4, A5; hence ( x in dom f & f . x in X ) by PARTFUN1:def_6; ::_thesis: verum end; assume that A6: x in dom f and A7: f . x in X ; ::_thesis: x in SC reconsider x1 = x as Element of C by A6; f /. x1 in X by A6, A7, PARTFUN1:def_6; hence x in SC by A4, A6; ::_thesis: verum end; hence SC = f " X by FUNCT_1:def_7; ::_thesis: verum end; theorem :: PARTFUN2:27 for D, C being non empty set for f being PartFunc of C,D ex g being Function of C,D st for c being Element of C st c in dom f holds g . c = f /. c proof let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D ex g being Function of C,D st for c being Element of C st c in dom f holds g . c = f /. c let f be PartFunc of C,D; ::_thesis: ex g being Function of C,D st for c being Element of C st c in dom f holds g . c = f /. c consider g being Function of C,D such that A1: for x being set st x in dom f holds g . x = f . x by FUNCT_2:71; take g ; ::_thesis: for c being Element of C st c in dom f holds g . c = f /. c let c be Element of C; ::_thesis: ( c in dom f implies g . c = f /. c ) assume A2: c in dom f ; ::_thesis: g . c = f /. c then g . c = f . c by A1; hence g . c = f /. c by A2, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:28 for D, C being non empty set for f, g being PartFunc of C,D holds ( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds f /. c = g /. c ) proof let D, C be non empty set ; ::_thesis: for f, g being PartFunc of C,D holds ( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds f /. c = g /. c ) let f, g be PartFunc of C,D; ::_thesis: ( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds f /. c = g /. c ) thus ( f tolerates g implies for c being Element of C st c in (dom f) /\ (dom g) holds f /. c = g /. c ) ::_thesis: ( ( for c being Element of C st c in (dom f) /\ (dom g) holds f /. c = g /. c ) implies f tolerates g ) proof assume A1: f tolerates g ; ::_thesis: for c being Element of C st c in (dom f) /\ (dom g) holds f /. c = g /. c let c be Element of C; ::_thesis: ( c in (dom f) /\ (dom g) implies f /. c = g /. c ) assume A2: c in (dom f) /\ (dom g) ; ::_thesis: f /. c = g /. c then A3: c in dom f by XBOOLE_0:def_4; f . c = g . c by A1, A2, PARTFUN1:def_4; then A4: f /. c = g . c by A3, PARTFUN1:def_6; c in dom g by A2, XBOOLE_0:def_4; hence f /. c = g /. c by A4, PARTFUN1:def_6; ::_thesis: verum end; assume A5: for c being Element of C st c in (dom f) /\ (dom g) holds f /. c = g /. c ; ::_thesis: f tolerates g now__::_thesis:_for_x_being_set_st_x_in_(dom_f)_/\_(dom_g)_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x ) assume A6: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x then reconsider x1 = x as Element of C ; ( x in dom f & f /. x1 = g /. x1 ) by A5, A6, XBOOLE_0:def_4; then A7: f . x = g /. x1 by PARTFUN1:def_6; x in dom g by A6, XBOOLE_0:def_4; hence f . x = g . x by A7, PARTFUN1:def_6; ::_thesis: verum end; hence f tolerates g by PARTFUN1:def_4; ::_thesis: verum end; scheme :: PARTFUN2:sch 1 PartFuncExD{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } : ex f being PartFunc of F1(),F2() st ( ( for d being Element of F1() holds ( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds P1[d,f /. d] ) ) proof defpred S1[ set ] means ex c being Element of F2() st P1[$1,c]; set x = the Element of F2(); defpred S2[ set , set ] means ( ( ex c being Element of F2() st P1[$1,c] implies P1[$1,$2] ) & ( ( for c being Element of F2() holds P1[$1,c] ) implies $2 = the Element of F2() ) ); consider X being set such that A1: for x being set holds ( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1(); for x being set st x in X holds x in F1() by A1; then reconsider X = X as Subset of F1() by TARSKI:def_3; A2: for d being Element of F1() ex z being Element of F2() st S2[d,z] proof let d be Element of F1(); ::_thesis: ex z being Element of F2() st S2[d,z] ( ( for c being Element of F2() holds P1[d,c] ) implies ex z being Element of F2() st ( ( ex c being Element of F2() st P1[d,c] implies P1[d,z] ) & ( ( for c being Element of F2() holds P1[d,c] ) implies z = the Element of F2() ) ) ) ; hence ex z being Element of F2() st S2[d,z] ; ::_thesis: verum end; consider g being Function of F1(),F2() such that A3: for d being Element of F1() holds S2[d,g . d] from FUNCT_2:sch_3(A2); reconsider f = g | X as PartFunc of F1(),F2() ; take f ; ::_thesis: ( ( for d being Element of F1() holds ( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds P1[d,f /. d] ) ) A4: dom g = F1() by FUNCT_2:def_1; thus for d being Element of F1() holds ( d in dom f iff ex c being Element of F2() st P1[d,c] ) ::_thesis: for d being Element of F1() st d in dom f holds P1[d,f /. d] proof let d be Element of F1(); ::_thesis: ( d in dom f iff ex c being Element of F2() st P1[d,c] ) dom f c= X by RELAT_1:58; hence ( d in dom f implies ex c being Element of F2() st P1[d,c] ) by A1; ::_thesis: ( ex c being Element of F2() st P1[d,c] implies d in dom f ) assume ex c being Element of F2() st P1[d,c] ; ::_thesis: d in dom f then d in X by A1; then d in (dom g) /\ X by A4, XBOOLE_0:def_4; hence d in dom f by RELAT_1:61; ::_thesis: verum end; let d be Element of F1(); ::_thesis: ( d in dom f implies P1[d,f /. d] ) assume A5: d in dom f ; ::_thesis: P1[d,f /. d] dom f c= X by RELAT_1:58; then ex c being Element of F2() st P1[d,c] by A1, A5; then P1[d,g . d] by A3; then P1[d,f . d] by A5, FUNCT_1:47; hence P1[d,f /. d] by A5, PARTFUN1:def_6; ::_thesis: verum end; scheme :: PARTFUN2:sch 2 LambdaPFD{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } : ex f being PartFunc of F1(),F2() st ( ( for d being Element of F1() holds ( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds f /. d = F3(d) ) ) proof defpred S1[ set , set ] means ( P1[$1] & $2 = F3($1) ); consider f being PartFunc of F1(),F2() such that A1: for d being Element of F1() holds ( d in dom f iff ex c being Element of F2() st S1[d,c] ) and A2: for d being Element of F1() st d in dom f holds S1[d,f /. d] from PARTFUN2:sch_1(); take f ; ::_thesis: ( ( for d being Element of F1() holds ( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds f /. d = F3(d) ) ) thus for d being Element of F1() holds ( d in dom f iff P1[d] ) ::_thesis: for d being Element of F1() st d in dom f holds f /. d = F3(d) proof let d be Element of F1(); ::_thesis: ( d in dom f iff P1[d] ) thus ( d in dom f implies P1[d] ) ::_thesis: ( P1[d] implies d in dom f ) proof assume d in dom f ; ::_thesis: P1[d] then ex c being Element of F2() st ( P1[d] & c = F3(d) ) by A1; hence P1[d] ; ::_thesis: verum end; assume P1[d] ; ::_thesis: d in dom f then ex c being Element of F2() st ( P1[d] & c = F3(d) ) ; hence d in dom f by A1; ::_thesis: verum end; thus for d being Element of F1() st d in dom f holds f /. d = F3(d) by A2; ::_thesis: verum end; scheme :: PARTFUN2:sch 3 UnPartFuncD{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4( set ) -> Element of F2() } : for f, g being PartFunc of F1(),F2() st dom f = F3() & ( for c being Element of F1() st c in dom f holds f /. c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds g /. c = F4(c) ) holds f = g proof let f, g be PartFunc of F1(),F2(); ::_thesis: ( dom f = F3() & ( for c being Element of F1() st c in dom f holds f /. c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds g /. c = F4(c) ) implies f = g ) assume that A1: dom f = F3() and A2: for c being Element of F1() st c in dom f holds f /. c = F4(c) and A3: dom g = F3() and A4: for c being Element of F1() st c in dom g holds g /. c = F4(c) ; ::_thesis: f = g now__::_thesis:_for_c_being_Element_of_F1()_st_c_in_dom_f_holds_ f_/._c_=_g_/._c let c be Element of F1(); ::_thesis: ( c in dom f implies f /. c = g /. c ) assume A5: c in dom f ; ::_thesis: f /. c = g /. c hence f /. c = F4(c) by A2 .= g /. c by A1, A3, A4, A5 ; ::_thesis: verum end; hence f = g by A1, A3, Th1; ::_thesis: verum end; definition let C, D be non empty set ; let SC be Subset of C; let d be Element of D; :: original: --> redefine funcSC --> d -> PartFunc of C,D; coherence SC --> d is PartFunc of C,D proof dom (SC --> d) = SC by FUNCOP_1:13; hence SC --> d is PartFunc of C,D by RELSET_1:7; ::_thesis: verum end; end; theorem Th29: :: PARTFUN2:29 for C, D being non empty set for SC being Subset of C for c being Element of C for d being Element of D st c in SC holds (SC --> d) /. c = d proof let C, D be non empty set ; ::_thesis: for SC being Subset of C for c being Element of C for d being Element of D st c in SC holds (SC --> d) /. c = d let SC be Subset of C; ::_thesis: for c being Element of C for d being Element of D st c in SC holds (SC --> d) /. c = d let c be Element of C; ::_thesis: for d being Element of D st c in SC holds (SC --> d) /. c = d let d be Element of D; ::_thesis: ( c in SC implies (SC --> d) /. c = d ) assume A1: c in SC ; ::_thesis: (SC --> d) /. c = d then ( dom (SC --> d) = SC & (SC --> d) . c = d ) by FUNCOP_1:7, FUNCOP_1:13; hence (SC --> d) /. c = d by A1, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:30 for D, C being non empty set for d being Element of D for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds f /. c = d ) holds f = (dom f) --> d proof let D, C be non empty set ; ::_thesis: for d being Element of D for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds f /. c = d ) holds f = (dom f) --> d let d be Element of D; ::_thesis: for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds f /. c = d ) holds f = (dom f) --> d let f be PartFunc of C,D; ::_thesis: ( ( for c being Element of C st c in dom f holds f /. c = d ) implies f = (dom f) --> d ) assume A1: for c being Element of C st c in dom f holds f /. c = d ; ::_thesis: f = (dom f) --> d now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_d let x be set ; ::_thesis: ( x in dom f implies f . x = d ) assume A2: x in dom f ; ::_thesis: f . x = d then reconsider x1 = x as Element of C ; f /. x1 = d by A1, A2; hence f . x = d by A2, PARTFUN1:def_6; ::_thesis: verum end; hence f = (dom f) --> d by FUNCOP_1:11; ::_thesis: verum end; theorem :: PARTFUN2:31 for E, C, D being non empty set for SE being Subset of E for c being Element of C for f being PartFunc of C,D st c in dom f holds f * (SE --> c) = SE --> (f /. c) proof let E, C, D be non empty set ; ::_thesis: for SE being Subset of E for c being Element of C for f being PartFunc of C,D st c in dom f holds f * (SE --> c) = SE --> (f /. c) let SE be Subset of E; ::_thesis: for c being Element of C for f being PartFunc of C,D st c in dom f holds f * (SE --> c) = SE --> (f /. c) let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in dom f holds f * (SE --> c) = SE --> (f /. c) let f be PartFunc of C,D; ::_thesis: ( c in dom f implies f * (SE --> c) = SE --> (f /. c) ) assume A1: c in dom f ; ::_thesis: f * (SE --> c) = SE --> (f /. c) then f * (SE --> c) = SE --> (f . c) by FUNCOP_1:17; hence f * (SE --> c) = SE --> (f /. c) by A1, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:32 for C being non empty set for SC being Subset of C holds ( id SC is total iff SC = C ) proof let C be non empty set ; ::_thesis: for SC being Subset of C holds ( id SC is total iff SC = C ) let SC be Subset of C; ::_thesis: ( id SC is total iff SC = C ) thus ( id SC is total implies SC = C ) ::_thesis: ( SC = C implies id SC is total ) proof assume id SC is total ; ::_thesis: SC = C then dom (id SC) = C by PARTFUN1:def_2; hence SC = C by RELAT_1:45; ::_thesis: verum end; assume SC = C ; ::_thesis: id SC is total then dom (id SC) = C by RELAT_1:45; hence id SC is total by PARTFUN1:def_2; ::_thesis: verum end; theorem :: PARTFUN2:33 for C, D being non empty set for SC being Subset of C for d being Element of D st SC --> d is total holds SC <> {} proof let C, D be non empty set ; ::_thesis: for SC being Subset of C for d being Element of D st SC --> d is total holds SC <> {} let SC be Subset of C; ::_thesis: for d being Element of D st SC --> d is total holds SC <> {} let d be Element of D; ::_thesis: ( SC --> d is total implies SC <> {} ) assume that A1: SC --> d is total and A2: SC = {} ; ::_thesis: contradiction dom (SC --> d) = C by A1, PARTFUN1:def_2; hence contradiction by A2, FUNCOP_1:10; ::_thesis: verum end; theorem :: PARTFUN2:34 for D, C being non empty set for SC being Subset of C for d being Element of D holds ( SC --> d is total iff SC = C ) proof let D, C be non empty set ; ::_thesis: for SC being Subset of C for d being Element of D holds ( SC --> d is total iff SC = C ) let SC be Subset of C; ::_thesis: for d being Element of D holds ( SC --> d is total iff SC = C ) let d be Element of D; ::_thesis: ( SC --> d is total iff SC = C ) thus ( SC --> d is total implies SC = C ) ::_thesis: ( SC = C implies SC --> d is total ) proof assume SC --> d is total ; ::_thesis: SC = C then dom (SC --> d) = C by PARTFUN1:def_2; hence SC = C by FUNCOP_1:13; ::_thesis: verum end; assume SC = C ; ::_thesis: SC --> d is total then dom (SC --> d) = C by FUNCOP_1:13; hence SC --> d is total by PARTFUN1:def_2; ::_thesis: verum end; definition let C, D be non empty set ; let f be PartFunc of C,D; :: original: constant redefine attrf is constant means :: PARTFUN2:def 1 ex d being Element of D st for c being Element of C st c in dom f holds f . c = d; compatibility ( f is constant iff ex d being Element of D st for c being Element of C st c in dom f holds f . c = d ) proof thus ( f is constant implies ex d being Element of D st for c being Element of C st c in dom f holds f . c = d ) ::_thesis: ( ex d being Element of D st for c being Element of C st c in dom f holds f . c = d implies f is constant ) proof assume A1: f is constant ; ::_thesis: ex d being Element of D st for c being Element of C st c in dom f holds f . c = d percases ( dom f = {} or dom f <> {} ) ; supposeA2: dom f = {} ; ::_thesis: ex d being Element of D st for c being Element of C st c in dom f holds f . c = d set d = the Element of D; take the Element of D ; ::_thesis: for c being Element of C st c in dom f holds f . c = the Element of D thus for c being Element of C st c in dom f holds f . c = the Element of D by A2; ::_thesis: verum end; suppose dom f <> {} ; ::_thesis: ex d being Element of D st for c being Element of C st c in dom f holds f . c = d then consider c0 being set such that A3: c0 in dom f by XBOOLE_0:def_1; reconsider c0 = c0 as Element of C by A3; take d = f /. c0; ::_thesis: for c being Element of C st c in dom f holds f . c = d let c be Element of C; ::_thesis: ( c in dom f implies f . c = d ) assume c in dom f ; ::_thesis: f . c = d hence f . c = f . c0 by A1, A3, FUNCT_1:def_10 .= d by A3, PARTFUN1:def_6 ; ::_thesis: verum end; end; end; given d being Element of D such that A4: for c being Element of C st c in dom f holds f . c = d ; ::_thesis: f is constant let x, y be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in dom f or not y in dom f or f . x = f . y ) assume that A5: x in dom f and A6: y in dom f ; ::_thesis: f . x = f . y thus f . x = d by A4, A5 .= f . y by A4, A6 ; ::_thesis: verum end; end; :: deftheorem defines constant PARTFUN2:def_1_:_ for C, D being non empty set for f being PartFunc of C,D holds ( f is constant iff ex d being Element of D st for c being Element of C st c in dom f holds f . c = d ); theorem Th35: :: PARTFUN2:35 for X being set for D, C being non empty set for f being PartFunc of C,D holds ( f | X is V8() iff ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f /. c = d ) proof let X be set ; ::_thesis: for D, C being non empty set for f being PartFunc of C,D holds ( f | X is V8() iff ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f /. c = d ) let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds ( f | X is V8() iff ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f /. c = d ) let f be PartFunc of C,D; ::_thesis: ( f | X is V8() iff ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f /. c = d ) thus ( f | X is V8() implies ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f /. c = d ) ::_thesis: ( ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f /. c = d implies f | X is V8() ) proof given d being Element of D such that A1: for c being Element of C st c in dom (f | X) holds (f | X) . c = d ; :: according to PARTFUN2:def_1 ::_thesis: ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f /. c = d take d ; ::_thesis: for c being Element of C st c in X /\ (dom f) holds f /. c = d let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f /. c = d ) assume A2: c in X /\ (dom f) ; ::_thesis: f /. c = d then A3: c in dom (f | X) by RELAT_1:61; c in dom f by A2, XBOOLE_0:def_4; hence f /. c = f . c by PARTFUN1:def_6 .= (f | X) . c by A3, FUNCT_1:47 .= d by A1, A3 ; ::_thesis: verum end; given d being Element of D such that A4: for c being Element of C st c in X /\ (dom f) holds f /. c = d ; ::_thesis: f | X is V8() take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom (f | X) holds (f | X) . c = d let c be Element of C; ::_thesis: ( c in dom (f | X) implies (f | X) . c = d ) assume A5: c in dom (f | X) ; ::_thesis: (f | X) . c = d then A6: c in X /\ (dom f) by RELAT_1:61; then A7: c in dom f by XBOOLE_0:def_4; thus (f | X) . c = f . c by A5, FUNCT_1:47 .= f /. c by A7, PARTFUN1:def_6 .= d by A4, A6 ; ::_thesis: verum end; theorem :: PARTFUN2:36 for X being set for D, C being non empty set for f being PartFunc of C,D holds ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f /. c1 = f /. c2 ) proof let X be set ; ::_thesis: for D, C being non empty set for f being PartFunc of C,D holds ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f /. c1 = f /. c2 ) let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f /. c1 = f /. c2 ) let f be PartFunc of C,D; ::_thesis: ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f /. c1 = f /. c2 ) thus ( f | X is V8() implies for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f /. c1 = f /. c2 ) ::_thesis: ( ( for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f /. c1 = f /. c2 ) implies f | X is V8() ) proof assume f | X is V8() ; ::_thesis: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f /. c1 = f /. c2 then consider d being Element of D such that A1: for c being Element of C st c in X /\ (dom f) holds f /. c = d by Th35; let c1, c2 be Element of C; ::_thesis: ( c1 in X /\ (dom f) & c2 in X /\ (dom f) implies f /. c1 = f /. c2 ) assume that A2: c1 in X /\ (dom f) and A3: c2 in X /\ (dom f) ; ::_thesis: f /. c1 = f /. c2 f /. c1 = d by A1, A2; hence f /. c1 = f /. c2 by A1, A3; ::_thesis: verum end; assume A4: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f /. c1 = f /. c2 ; ::_thesis: f | X is V8() now__::_thesis:_f_|_X_is_V8() percases ( X /\ (dom f) = {} or X /\ (dom f) <> {} ) ; supposeA5: X /\ (dom f) = {} ; ::_thesis: f | X is V8() now__::_thesis:_ex_d_being_Element_of_D_st_ for_c_being_Element_of_C_st_c_in_X_/\_(dom_f)_holds_ f_/._c_=_d set d = the Element of D; take d = the Element of D; ::_thesis: for c being Element of C st c in X /\ (dom f) holds f /. c = d let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f /. c = d ) thus ( c in X /\ (dom f) implies f /. c = d ) by A5; ::_thesis: verum end; hence f | X is V8() by Th35; ::_thesis: verum end; supposeA6: X /\ (dom f) <> {} ; ::_thesis: f | X is V8() set x = the Element of X /\ (dom f); the Element of X /\ (dom f) in dom f by A6, XBOOLE_0:def_4; then reconsider x = the Element of X /\ (dom f) as Element of C ; for c being Element of C st c in X /\ (dom f) holds f /. c = f /. x by A4; hence f | X is V8() by Th35; ::_thesis: verum end; end; end; hence f | X is V8() ; ::_thesis: verum end; theorem :: PARTFUN2:37 for X being set for C, D being non empty set for f being PartFunc of C,D st X meets dom f holds ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} ) proof let X be set ; ::_thesis: for C, D being non empty set for f being PartFunc of C,D st X meets dom f holds ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} ) let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st X meets dom f holds ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} ) let f be PartFunc of C,D; ::_thesis: ( X meets dom f implies ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} ) ) assume A1: X /\ (dom f) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} ) thus ( f | X is V8() implies ex d being Element of D st rng (f | X) = {d} ) ::_thesis: ( ex d being Element of D st rng (f | X) = {d} implies f | X is V8() ) proof assume f | X is V8() ; ::_thesis: ex d being Element of D st rng (f | X) = {d} then consider d being Element of D such that A2: for c being Element of C st c in X /\ (dom f) holds f /. c = d by Th35; take d ; ::_thesis: rng (f | X) = {d} thus rng (f | X) c= {d} :: according to XBOOLE_0:def_10 ::_thesis: {d} c= rng (f | X) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f | X) or x in {d} ) assume x in rng (f | X) ; ::_thesis: x in {d} then consider y being set such that A3: y in dom (f | X) and A4: (f | X) . y = x by FUNCT_1:def_3; reconsider y = y as Element of C by A3; dom (f | X) = X /\ (dom f) by RELAT_1:61; then d = f /. y by A2, A3 .= (f | X) /. y by A3, Th15 .= x by A3, A4, PARTFUN1:def_6 ; hence x in {d} by TARSKI:def_1; ::_thesis: verum end; thus {d} c= rng (f | X) ::_thesis: verum proof set y = the Element of X /\ (dom f); the Element of X /\ (dom f) in dom f by A1, XBOOLE_0:def_4; then reconsider y = the Element of X /\ (dom f) as Element of C ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {d} or x in rng (f | X) ) assume A5: x in {d} ; ::_thesis: x in rng (f | X) A6: dom (f | X) = X /\ (dom f) by RELAT_1:61; then (f | X) /. y = f /. y by A1, Th15 .= d by A1, A2 .= x by A5, TARSKI:def_1 ; hence x in rng (f | X) by A1, A6, Th2; ::_thesis: verum end; end; given d being Element of D such that A7: rng (f | X) = {d} ; ::_thesis: f | X is V8() take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom (f | X) holds (f | X) . c = d let c be Element of C; ::_thesis: ( c in dom (f | X) implies (f | X) . c = d ) assume A8: c in dom (f | X) ; ::_thesis: (f | X) . c = d then (f | X) /. c in {d} by A7, Th2; then (f | X) . c in {d} by A8, PARTFUN1:def_6; hence (f | X) . c = d by TARSKI:def_1; ::_thesis: verum end; theorem :: PARTFUN2:38 for X, Y being set for C, D being non empty set for f being PartFunc of C,D st f | X is V8() & Y c= X holds f | Y is V8() proof let X, Y be set ; ::_thesis: for C, D being non empty set for f being PartFunc of C,D st f | X is V8() & Y c= X holds f | Y is V8() let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st f | X is V8() & Y c= X holds f | Y is V8() let f be PartFunc of C,D; ::_thesis: ( f | X is V8() & Y c= X implies f | Y is V8() ) assume that A1: f | X is V8() and A2: Y c= X ; ::_thesis: f | Y is V8() consider d being Element of D such that A3: for c being Element of C st c in X /\ (dom f) holds f /. c = d by A1, Th35; now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_f)_holds_ f_/._c_=_d let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies f /. c = d ) assume c in Y /\ (dom f) ; ::_thesis: f /. c = d then ( c in Y & c in dom f ) by XBOOLE_0:def_4; then c in X /\ (dom f) by A2, XBOOLE_0:def_4; hence f /. c = d by A3; ::_thesis: verum end; hence f | Y is V8() by Th35; ::_thesis: verum end; theorem Th39: :: PARTFUN2:39 for X being set for C, D being non empty set for f being PartFunc of C,D st X misses dom f holds f | X is V8() proof let X be set ; ::_thesis: for C, D being non empty set for f being PartFunc of C,D st X misses dom f holds f | X is V8() let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st X misses dom f holds f | X is V8() let f be PartFunc of C,D; ::_thesis: ( X misses dom f implies f | X is V8() ) assume A1: X /\ (dom f) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f | X is V8() now__::_thesis:_ex_d_being_Element_of_D_st_ for_c_being_Element_of_C_st_c_in_X_/\_(dom_f)_holds_ f_/._c_=_d set d = the Element of D; take d = the Element of D; ::_thesis: for c being Element of C st c in X /\ (dom f) holds f /. c = d let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f /. c = d ) thus ( c in X /\ (dom f) implies f /. c = d ) by A1; ::_thesis: verum end; hence f | X is V8() by Th35; ::_thesis: verum end; theorem :: PARTFUN2:40 for C, D being non empty set for SC being Subset of C for d being Element of D for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds f | SC is V8() proof let C, D be non empty set ; ::_thesis: for SC being Subset of C for d being Element of D for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds f | SC is V8() let SC be Subset of C; ::_thesis: for d being Element of D for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds f | SC is V8() let d be Element of D; ::_thesis: for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds f | SC is V8() let f be PartFunc of C,D; ::_thesis: ( f | SC = (dom (f | SC)) --> d implies f | SC is V8() ) assume A1: f | SC = (dom (f | SC)) --> d ; ::_thesis: f | SC is V8() now__::_thesis:_for_c_being_Element_of_C_st_c_in_SC_/\_(dom_f)_holds_ f_/._c_=_d let c be Element of C; ::_thesis: ( c in SC /\ (dom f) implies f /. c = d ) assume c in SC /\ (dom f) ; ::_thesis: f /. c = d then A2: c in dom (f | SC) by RELAT_1:61; then (f | SC) /. c = d by A1, Th29; hence f /. c = d by A2, Th15; ::_thesis: verum end; hence f | SC is V8() by Th35; ::_thesis: verum end; theorem :: PARTFUN2:41 for x being set for C, D being non empty set for f being PartFunc of C,D holds f | {x} is V8() proof let x be set ; ::_thesis: for C, D being non empty set for f being PartFunc of C,D holds f | {x} is V8() let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D holds f | {x} is V8() let f be PartFunc of C,D; ::_thesis: f | {x} is V8() now__::_thesis:_f_|_{x}_is_V8() percases ( {x} /\ (dom f) = {} or {x} /\ (dom f) <> {} ) ; suppose {x} /\ (dom f) = {} ; ::_thesis: f | {x} is V8() then {x} misses dom f by XBOOLE_0:def_7; hence f | {x} is V8() by Th39; ::_thesis: verum end; supposeA1: {x} /\ (dom f) <> {} ; ::_thesis: f | {x} is V8() set y = the Element of {x} /\ (dom f); ( the Element of {x} /\ (dom f) in {x} & the Element of {x} /\ (dom f) in dom f ) by A1, XBOOLE_0:def_4; then reconsider x1 = x as Element of C by TARSKI:def_1; now__::_thesis:_ex_d_being_Element_of_D_st_ for_c_being_Element_of_C_st_c_in_{x}_/\_(dom_f)_holds_ f_/._c_=_f_/._x1 take d = f /. x1; ::_thesis: for c being Element of C st c in {x} /\ (dom f) holds f /. c = f /. x1 let c be Element of C; ::_thesis: ( c in {x} /\ (dom f) implies f /. c = f /. x1 ) assume c in {x} /\ (dom f) ; ::_thesis: f /. c = f /. x1 then c in {x} by XBOOLE_0:def_4; hence f /. c = f /. x1 by TARSKI:def_1; ::_thesis: verum end; hence f | {x} is V8() by Th35; ::_thesis: verum end; end; end; hence f | {x} is V8() ; ::_thesis: verum end; theorem :: PARTFUN2:42 for X, Y being set for C, D being non empty set for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds f | (X \/ Y) is V8() proof let X, Y be set ; ::_thesis: for C, D being non empty set for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds f | (X \/ Y) is V8() let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds f | (X \/ Y) is V8() let f be PartFunc of C,D; ::_thesis: ( f | X is V8() & f | Y is V8() & X /\ Y meets dom f implies f | (X \/ Y) is V8() ) assume that A1: f | X is V8() and A2: f | Y is V8() and A3: (X /\ Y) /\ (dom f) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: f | (X \/ Y) is V8() consider d1 being Element of D such that A4: for c being Element of C st c in X /\ (dom f) holds f /. c = d1 by A1, Th35; set x = the Element of (X /\ Y) /\ (dom f); A5: the Element of (X /\ Y) /\ (dom f) in X /\ Y by A3, XBOOLE_0:def_4; A6: the Element of (X /\ Y) /\ (dom f) in dom f by A3, XBOOLE_0:def_4; then reconsider x = the Element of (X /\ Y) /\ (dom f) as Element of C ; x in Y by A5, XBOOLE_0:def_4; then A7: x in Y /\ (dom f) by A6, XBOOLE_0:def_4; consider d2 being Element of D such that A8: for c being Element of C st c in Y /\ (dom f) holds f /. c = d2 by A2, Th35; x in X by A5, XBOOLE_0:def_4; then x in X /\ (dom f) by A6, XBOOLE_0:def_4; then f /. x = d1 by A4; then A9: d1 = d2 by A8, A7; take d1 ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom (f | (X \/ Y)) holds (f | (X \/ Y)) . c = d1 let c be Element of C; ::_thesis: ( c in dom (f | (X \/ Y)) implies (f | (X \/ Y)) . c = d1 ) assume A10: c in dom (f | (X \/ Y)) ; ::_thesis: (f | (X \/ Y)) . c = d1 then A11: c in (X \/ Y) /\ (dom f) by RELAT_1:61; then A12: c in dom f by XBOOLE_0:def_4; A13: c in X \/ Y by A11, XBOOLE_0:def_4; now__::_thesis:_f_/._c_=_d1 percases ( c in X or c in Y ) by A13, XBOOLE_0:def_3; suppose c in X ; ::_thesis: f /. c = d1 then c in X /\ (dom f) by A12, XBOOLE_0:def_4; hence f /. c = d1 by A4; ::_thesis: verum end; suppose c in Y ; ::_thesis: f /. c = d1 then c in Y /\ (dom f) by A12, XBOOLE_0:def_4; hence f /. c = d1 by A8, A9; ::_thesis: verum end; end; end; then (f | (X \/ Y)) /. c = d1 by A11, Th16; hence (f | (X \/ Y)) . c = d1 by A10, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:43 for Y, X being set for C, D being non empty set for f being PartFunc of C,D st f | Y is V8() holds (f | X) | Y is V8() proof let Y, X be set ; ::_thesis: for C, D being non empty set for f being PartFunc of C,D st f | Y is V8() holds (f | X) | Y is V8() let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st f | Y is V8() holds (f | X) | Y is V8() let f be PartFunc of C,D; ::_thesis: ( f | Y is V8() implies (f | X) | Y is V8() ) assume f | Y is V8() ; ::_thesis: (f | X) | Y is V8() then consider d being Element of D such that A1: for c being Element of C st c in Y /\ (dom f) holds f /. c = d by Th35; take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom ((f | X) | Y) holds ((f | X) | Y) . c = d let c be Element of C; ::_thesis: ( c in dom ((f | X) | Y) implies ((f | X) | Y) . c = d ) assume A2: c in dom ((f | X) | Y) ; ::_thesis: ((f | X) | Y) . c = d then A3: c in Y /\ (dom (f | X)) by RELAT_1:61; then A4: c in Y by XBOOLE_0:def_4; A5: c in dom (f | X) by A3, XBOOLE_0:def_4; then c in (dom f) /\ X by RELAT_1:61; then c in dom f by XBOOLE_0:def_4; then c in Y /\ (dom f) by A4, XBOOLE_0:def_4; then f /. c = d by A1; then (f | X) /. c = d by A5, Th15; then ((f | X) | Y) /. c = d by A3, Th16; hence ((f | X) | Y) . c = d by A2, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:44 for C, D being non empty set for SC being Subset of C for d being Element of D holds (SC --> d) | SC is V8() proof let C, D be non empty set ; ::_thesis: for SC being Subset of C for d being Element of D holds (SC --> d) | SC is V8() let SC be Subset of C; ::_thesis: for d being Element of D holds (SC --> d) | SC is V8() let d be Element of D; ::_thesis: (SC --> d) | SC is V8() take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom ((SC --> d) | SC) holds ((SC --> d) | SC) . c = d let c be Element of C; ::_thesis: ( c in dom ((SC --> d) | SC) implies ((SC --> d) | SC) . c = d ) assume A1: c in dom ((SC --> d) | SC) ; ::_thesis: ((SC --> d) | SC) . c = d then A2: c in SC /\ (dom (SC --> d)) by RELAT_1:61; then c in SC by XBOOLE_0:def_4; then (SC --> d) /. c = d by Th29; then ((SC --> d) | SC) /. c = d by A2, Th16; hence ((SC --> d) | SC) . c = d by A1, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:45 for D, C being non empty set for f, g being PartFunc of C,D st dom f c= dom g & ( for c being Element of C st c in dom f holds f /. c = g /. c ) holds f c= g proof let D, C be non empty set ; ::_thesis: for f, g being PartFunc of C,D st dom f c= dom g & ( for c being Element of C st c in dom f holds f /. c = g /. c ) holds f c= g let f, g be PartFunc of C,D; ::_thesis: ( dom f c= dom g & ( for c being Element of C st c in dom f holds f /. c = g /. c ) implies f c= g ) assume that A1: dom f c= dom g and A2: for c being Element of C st c in dom f holds f /. c = g /. c ; ::_thesis: f c= g now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in dom f implies f . x = g . x ) assume A3: x in dom f ; ::_thesis: f . x = g . x then reconsider x1 = x as Element of C ; f /. x1 = g /. x1 by A2, A3; then f . x = g /. x1 by A3, PARTFUN1:def_6; hence f . x = g . x by A1, A3, PARTFUN1:def_6; ::_thesis: verum end; hence f c= g by A1, GRFUNC_1:2; ::_thesis: verum end; theorem Th46: :: PARTFUN2:46 for C, D being non empty set for c being Element of C for d being Element of D for f being PartFunc of C,D holds ( ( c in dom f & d = f /. c ) iff [c,d] in f ) proof let C, D be non empty set ; ::_thesis: for c being Element of C for d being Element of D for f being PartFunc of C,D holds ( ( c in dom f & d = f /. c ) iff [c,d] in f ) let c be Element of C; ::_thesis: for d being Element of D for f being PartFunc of C,D holds ( ( c in dom f & d = f /. c ) iff [c,d] in f ) let d be Element of D; ::_thesis: for f being PartFunc of C,D holds ( ( c in dom f & d = f /. c ) iff [c,d] in f ) let f be PartFunc of C,D; ::_thesis: ( ( c in dom f & d = f /. c ) iff [c,d] in f ) thus ( c in dom f & d = f /. c implies [c,d] in f ) ::_thesis: ( [c,d] in f implies ( c in dom f & d = f /. c ) ) proof assume that A1: c in dom f and A2: d = f /. c ; ::_thesis: [c,d] in f d = f . c by A1, A2, PARTFUN1:def_6; hence [c,d] in f by A1, FUNCT_1:1; ::_thesis: verum end; assume [c,d] in f ; ::_thesis: ( c in dom f & d = f /. c ) then ( c in dom f & d = f . c ) by FUNCT_1:1; hence ( c in dom f & d = f /. c ) by PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:47 for C, D, E being non empty set for c being Element of C for e being Element of E for f being PartFunc of C,D for s being PartFunc of D,E st [c,e] in s * f holds ( [c,(f /. c)] in f & [(f /. c),e] in s ) proof let C, D, E be non empty set ; ::_thesis: for c being Element of C for e being Element of E for f being PartFunc of C,D for s being PartFunc of D,E st [c,e] in s * f holds ( [c,(f /. c)] in f & [(f /. c),e] in s ) let c be Element of C; ::_thesis: for e being Element of E for f being PartFunc of C,D for s being PartFunc of D,E st [c,e] in s * f holds ( [c,(f /. c)] in f & [(f /. c),e] in s ) let e be Element of E; ::_thesis: for f being PartFunc of C,D for s being PartFunc of D,E st [c,e] in s * f holds ( [c,(f /. c)] in f & [(f /. c),e] in s ) let f be PartFunc of C,D; ::_thesis: for s being PartFunc of D,E st [c,e] in s * f holds ( [c,(f /. c)] in f & [(f /. c),e] in s ) let s be PartFunc of D,E; ::_thesis: ( [c,e] in s * f implies ( [c,(f /. c)] in f & [(f /. c),e] in s ) ) assume A1: [c,e] in s * f ; ::_thesis: ( [c,(f /. c)] in f & [(f /. c),e] in s ) then A2: [(f . c),e] in s by GRFUNC_1:4; A3: [c,(f . c)] in f by A1, GRFUNC_1:4; then c in dom f by FUNCT_1:1; hence ( [c,(f /. c)] in f & [(f /. c),e] in s ) by A3, A2, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:48 for C, D being non empty set for c being Element of C for d being Element of D for f being PartFunc of C,D st f = {[c,d]} holds f /. c = d proof let C, D be non empty set ; ::_thesis: for c being Element of C for d being Element of D for f being PartFunc of C,D st f = {[c,d]} holds f /. c = d let c be Element of C; ::_thesis: for d being Element of D for f being PartFunc of C,D st f = {[c,d]} holds f /. c = d let d be Element of D; ::_thesis: for f being PartFunc of C,D st f = {[c,d]} holds f /. c = d let f be PartFunc of C,D; ::_thesis: ( f = {[c,d]} implies f /. c = d ) assume A1: f = {[c,d]} ; ::_thesis: f /. c = d then [c,d] in f by TARSKI:def_1; then A2: c in dom f by FUNCT_1:1; f . c = d by A1, GRFUNC_1:6; hence f /. c = d by A2, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:49 for C, D being non empty set for c being Element of C for f being PartFunc of C,D st dom f = {c} holds f = {[c,(f /. c)]} proof let C, D be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,D st dom f = {c} holds f = {[c,(f /. c)]} let c be Element of C; ::_thesis: for f being PartFunc of C,D st dom f = {c} holds f = {[c,(f /. c)]} let f be PartFunc of C,D; ::_thesis: ( dom f = {c} implies f = {[c,(f /. c)]} ) assume dom f = {c} ; ::_thesis: f = {[c,(f /. c)]} then ( c in dom f & f = {[c,(f . c)]} ) by GRFUNC_1:7, TARSKI:def_1; hence f = {[c,(f /. c)]} by PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:50 for C, D being non empty set for c being Element of C for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds ( f1 /. c = f /. c & f1 /. c = g /. c ) proof let C, D be non empty set ; ::_thesis: for c being Element of C for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds ( f1 /. c = f /. c & f1 /. c = g /. c ) let c be Element of C; ::_thesis: for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds ( f1 /. c = f /. c & f1 /. c = g /. c ) let f1, f, g be PartFunc of C,D; ::_thesis: ( f1 = f /\ g & c in dom f1 implies ( f1 /. c = f /. c & f1 /. c = g /. c ) ) assume that A1: f1 = f /\ g and A2: c in dom f1 ; ::_thesis: ( f1 /. c = f /. c & f1 /. c = g /. c ) f1 . c = g . c by A1, A2, GRFUNC_1:11; then A3: f1 /. c = g . c by A2, PARTFUN1:def_6; A4: [c,(f1 . c)] in f1 by A2, FUNCT_1:1; then [c,(f1 . c)] in f by A1, XBOOLE_0:def_4; then A5: c in dom f by FUNCT_1:1; [c,(f1 . c)] in g by A1, A4, XBOOLE_0:def_4; then A6: c in dom g by FUNCT_1:1; f1 . c = f . c by A1, A2, GRFUNC_1:11; then f1 /. c = f . c by A2, PARTFUN1:def_6; hence ( f1 /. c = f /. c & f1 /. c = g /. c ) by A5, A6, A3, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:51 for C, D being non empty set for c being Element of C for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds f1 /. c = f /. c proof let C, D be non empty set ; ::_thesis: for c being Element of C for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds f1 /. c = f /. c let c be Element of C; ::_thesis: for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds f1 /. c = f /. c let f, f1, g be PartFunc of C,D; ::_thesis: ( c in dom f & f1 = f \/ g implies f1 /. c = f /. c ) assume that A1: c in dom f and A2: f1 = f \/ g ; ::_thesis: f1 /. c = f /. c [c,(f . c)] in f by A1, FUNCT_1:1; then [c,(f . c)] in f1 by A2, XBOOLE_0:def_3; then A3: c in dom f1 by FUNCT_1:1; f1 . c = f . c by A1, A2, GRFUNC_1:15; then f1 /. c = f . c by A3, PARTFUN1:def_6; hence f1 /. c = f /. c by A1, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:52 for C, D being non empty set for c being Element of C for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds f1 /. c = g /. c proof let C, D be non empty set ; ::_thesis: for c being Element of C for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds f1 /. c = g /. c let c be Element of C; ::_thesis: for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds f1 /. c = g /. c let g, f1, f be PartFunc of C,D; ::_thesis: ( c in dom g & f1 = f \/ g implies f1 /. c = g /. c ) assume that A1: c in dom g and A2: f1 = f \/ g ; ::_thesis: f1 /. c = g /. c [c,(g . c)] in g by A1, FUNCT_1:1; then [c,(g . c)] in f1 by A2, XBOOLE_0:def_3; then A3: c in dom f1 by FUNCT_1:1; f1 . c = g . c by A1, A2, GRFUNC_1:15; then f1 /. c = g . c by A3, PARTFUN1:def_6; hence f1 /. c = g /. c by A1, PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:53 for C, D being non empty set for c being Element of C for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds f1 /. c = g /. c proof let C, D be non empty set ; ::_thesis: for c being Element of C for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds f1 /. c = g /. c let c be Element of C; ::_thesis: for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds f1 /. c = g /. c let f1, f, g be PartFunc of C,D; ::_thesis: ( c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c implies f1 /. c = g /. c ) assume that A1: c in dom f1 and A2: f1 = f \/ g ; ::_thesis: ( f1 /. c = f /. c or f1 /. c = g /. c ) [c,(f1 /. c)] in f1 by A1, Th46; then A3: ( [c,(f1 /. c)] in f or [c,(f1 /. c)] in g ) by A2, XBOOLE_0:def_3; now__::_thesis:_(_f1_/._c_=_f_/._c_or_f1_/._c_=_g_/._c_) percases ( c in dom f or c in dom g ) by A3, FUNCT_1:1; suppose c in dom f ; ::_thesis: ( f1 /. c = f /. c or f1 /. c = g /. c ) then [c,(f /. c)] in f by Th46; then [c,(f /. c)] in f1 by A2, XBOOLE_0:def_3; hence ( f1 /. c = f /. c or f1 /. c = g /. c ) by Th46; ::_thesis: verum end; suppose c in dom g ; ::_thesis: ( f1 /. c = f /. c or f1 /. c = g /. c ) then [c,(g /. c)] in g by Th46; then [c,(g /. c)] in f1 by A2, XBOOLE_0:def_3; hence ( f1 /. c = f /. c or f1 /. c = g /. c ) by Th46; ::_thesis: verum end; end; end; hence ( f1 /. c = f /. c or f1 /. c = g /. c ) ; ::_thesis: verum end; theorem :: PARTFUN2:54 for C, D being non empty set for SC being Subset of C for c being Element of C for f being PartFunc of C,D holds ( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC ) proof let C, D be non empty set ; ::_thesis: for SC being Subset of C for c being Element of C for f being PartFunc of C,D holds ( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC ) let SC be Subset of C; ::_thesis: for c being Element of C for f being PartFunc of C,D holds ( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC ) let c be Element of C; ::_thesis: for f being PartFunc of C,D holds ( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC ) let f be PartFunc of C,D; ::_thesis: ( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC ) thus ( c in dom f & c in SC implies [c,(f /. c)] in f | SC ) ::_thesis: ( [c,(f /. c)] in f | SC implies ( c in dom f & c in SC ) ) proof assume that A1: c in dom f and A2: c in SC ; ::_thesis: [c,(f /. c)] in f | SC [c,(f . c)] in f | SC by A1, A2, GRFUNC_1:22; hence [c,(f /. c)] in f | SC by A1, PARTFUN1:def_6; ::_thesis: verum end; assume [c,(f /. c)] in f | SC ; ::_thesis: ( c in dom f & c in SC ) then c in dom (f | SC) by FUNCT_1:1; then c in (dom f) /\ SC by RELAT_1:61; hence ( c in dom f & c in SC ) by XBOOLE_0:def_4; ::_thesis: verum end; theorem :: PARTFUN2:55 for C, D being non empty set for SD being Subset of D for c being Element of C for f being PartFunc of C,D holds ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f ) proof let C, D be non empty set ; ::_thesis: for SD being Subset of D for c being Element of C for f being PartFunc of C,D holds ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f ) let SD be Subset of D; ::_thesis: for c being Element of C for f being PartFunc of C,D holds ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f ) let c be Element of C; ::_thesis: for f being PartFunc of C,D holds ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f ) let f be PartFunc of C,D; ::_thesis: ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f ) thus ( c in dom f & f /. c in SD implies [c,(f /. c)] in SD |` f ) ::_thesis: ( [c,(f /. c)] in SD |` f implies ( c in dom f & f /. c in SD ) ) proof assume that A1: c in dom f and A2: f /. c in SD ; ::_thesis: [c,(f /. c)] in SD |` f f . c in SD by A1, A2, PARTFUN1:def_6; then [c,(f . c)] in SD |` f by A1, GRFUNC_1:24; hence [c,(f /. c)] in SD |` f by A1, PARTFUN1:def_6; ::_thesis: verum end; assume [c,(f /. c)] in SD |` f ; ::_thesis: ( c in dom f & f /. c in SD ) then c in dom (SD |` f) by FUNCT_1:1; then ( c in dom f & f . c in SD ) by FUNCT_1:54; hence ( c in dom f & f /. c in SD ) by PARTFUN1:def_6; ::_thesis: verum end; theorem :: PARTFUN2:56 for C, D being non empty set for SD being Subset of D for c being Element of C for f being PartFunc of C,D holds ( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) ) proof let C, D be non empty set ; ::_thesis: for SD being Subset of D for c being Element of C for f being PartFunc of C,D holds ( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) ) let SD be Subset of D; ::_thesis: for c being Element of C for f being PartFunc of C,D holds ( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) ) let c be Element of C; ::_thesis: for f being PartFunc of C,D holds ( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) ) let f be PartFunc of C,D; ::_thesis: ( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) ) thus ( c in f " SD implies ( [c,(f /. c)] in f & f /. c in SD ) ) ::_thesis: ( [c,(f /. c)] in f & f /. c in SD implies c in f " SD ) proof assume A1: c in f " SD ; ::_thesis: ( [c,(f /. c)] in f & f /. c in SD ) then A2: f . c in SD by GRFUNC_1:26; A3: [c,(f . c)] in f by A1, GRFUNC_1:26; then c in dom f by FUNCT_1:1; hence ( [c,(f /. c)] in f & f /. c in SD ) by A3, A2, PARTFUN1:def_6; ::_thesis: verum end; assume that A4: [c,(f /. c)] in f and A5: f /. c in SD ; ::_thesis: c in f " SD c in dom f by A4, Th46; hence c in f " SD by A5, Th26; ::_thesis: verum end; theorem Th57: :: PARTFUN2:57 for X being set for D, C being non empty set for f being PartFunc of C,D holds ( f | X is V8() iff ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f . c = d ) proof let X be set ; ::_thesis: for D, C being non empty set for f being PartFunc of C,D holds ( f | X is V8() iff ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f . c = d ) let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds ( f | X is V8() iff ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f . c = d ) let f be PartFunc of C,D; ::_thesis: ( f | X is V8() iff ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f . c = d ) hereby ::_thesis: ( ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f . c = d implies f | X is V8() ) assume f | X is V8() ; ::_thesis: ex d being Element of D st for c being Element of C st c in X /\ (dom f) holds f . c = d then consider d being Element of D such that A1: for c being Element of C st c in X /\ (dom f) holds f /. c = d by Th35; take d = d; ::_thesis: for c being Element of C st c in X /\ (dom f) holds f . c = d let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f . c = d ) assume A2: c in X /\ (dom f) ; ::_thesis: f . c = d then c in dom f by XBOOLE_0:def_4; hence f . c = f /. c by PARTFUN1:def_6 .= d by A1, A2 ; ::_thesis: verum end; given d being Element of D such that A3: for c being Element of C st c in X /\ (dom f) holds f . c = d ; ::_thesis: f | X is V8() take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom (f | X) holds (f | X) . c = d let c be Element of C; ::_thesis: ( c in dom (f | X) implies (f | X) . c = d ) assume A4: c in dom (f | X) ; ::_thesis: (f | X) . c = d then A5: c in X /\ (dom f) by RELAT_1:61; then A6: c in dom f by XBOOLE_0:def_4; thus (f | X) . c = (f | X) /. c by A4, PARTFUN1:def_6 .= f /. c by A5, Th16 .= f . c by A6, PARTFUN1:def_6 .= d by A3, A5 ; ::_thesis: verum end; theorem :: PARTFUN2:58 for X being set for D, C being non empty set for f being PartFunc of C,D holds ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f . c1 = f . c2 ) proof let X be set ; ::_thesis: for D, C being non empty set for f being PartFunc of C,D holds ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f . c1 = f . c2 ) let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f . c1 = f . c2 ) let f be PartFunc of C,D; ::_thesis: ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f . c1 = f . c2 ) thus ( f | X is V8() implies for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f . c1 = f . c2 ) ::_thesis: ( ( for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f . c1 = f . c2 ) implies f | X is V8() ) proof assume f | X is V8() ; ::_thesis: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f . c1 = f . c2 then consider d being Element of D such that A1: for c being Element of C st c in X /\ (dom f) holds f . c = d by Th57; let c1, c2 be Element of C; ::_thesis: ( c1 in X /\ (dom f) & c2 in X /\ (dom f) implies f . c1 = f . c2 ) assume that A2: c1 in X /\ (dom f) and A3: c2 in X /\ (dom f) ; ::_thesis: f . c1 = f . c2 f . c1 = d by A1, A2; hence f . c1 = f . c2 by A1, A3; ::_thesis: verum end; assume A4: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds f . c1 = f . c2 ; ::_thesis: f | X is V8() now__::_thesis:_f_|_X_is_V8() percases ( X /\ (dom f) = {} or X /\ (dom f) <> {} ) ; supposeA5: X /\ (dom f) = {} ; ::_thesis: f | X is V8() now__::_thesis:_ex_d_being_Element_of_D_st_ for_c_being_Element_of_C_st_c_in_X_/\_(dom_f)_holds_ f_._c_=_d set d = the Element of D; take d = the Element of D; ::_thesis: for c being Element of C st c in X /\ (dom f) holds f . c = d let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f . c = d ) thus ( c in X /\ (dom f) implies f . c = d ) by A5; ::_thesis: verum end; hence f | X is V8() by Th57; ::_thesis: verum end; supposeA6: X /\ (dom f) <> {} ; ::_thesis: f | X is V8() set x = the Element of X /\ (dom f); now__::_thesis:_for_c_being_Element_of_C_st_c_in_X_/\_(dom_f)_holds_ f_._c_=_f_/._the_Element_of_X_/\_(dom_f) let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f . c = f /. the Element of X /\ (dom f) ) A7: the Element of X /\ (dom f) in dom f by A6, XBOOLE_0:def_4; assume c in X /\ (dom f) ; ::_thesis: f . c = f /. the Element of X /\ (dom f) hence f . c = f . the Element of X /\ (dom f) by A4, A7 .= f /. the Element of X /\ (dom f) by A7, PARTFUN1:def_6 ; ::_thesis: verum end; hence f | X is V8() by Th57; ::_thesis: verum end; end; end; hence f | X is V8() ; ::_thesis: verum end; theorem :: PARTFUN2:59 for X being set for D, C being non empty set for d being Element of D for f being PartFunc of C,D st d in f .: X holds ex c being Element of C st ( c in dom f & c in X & d = f . c ) proof let X be set ; ::_thesis: for D, C being non empty set for d being Element of D for f being PartFunc of C,D st d in f .: X holds ex c being Element of C st ( c in dom f & c in X & d = f . c ) let D, C be non empty set ; ::_thesis: for d being Element of D for f being PartFunc of C,D st d in f .: X holds ex c being Element of C st ( c in dom f & c in X & d = f . c ) let d be Element of D; ::_thesis: for f being PartFunc of C,D st d in f .: X holds ex c being Element of C st ( c in dom f & c in X & d = f . c ) let f be PartFunc of C,D; ::_thesis: ( d in f .: X implies ex c being Element of C st ( c in dom f & c in X & d = f . c ) ) assume d in f .: X ; ::_thesis: ex c being Element of C st ( c in dom f & c in X & d = f . c ) then consider x being set such that A1: x in dom f and A2: ( x in X & d = f . x ) by FUNCT_1:def_6; reconsider x = x as Element of C by A1; take x ; ::_thesis: ( x in dom f & x in X & d = f . x ) thus ( x in dom f & x in X & d = f . x ) by A1, A2; ::_thesis: verum end; theorem :: PARTFUN2:60 for C, D being non empty set for c being Element of C for d being Element of D for f being PartFunc of C,D st f is one-to-one holds ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) proof let C, D be non empty set ; ::_thesis: for c being Element of C for d being Element of D for f being PartFunc of C,D st f is one-to-one holds ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) let c be Element of C; ::_thesis: for d being Element of D for f being PartFunc of C,D st f is one-to-one holds ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) let d be Element of D; ::_thesis: for f being PartFunc of C,D st f is one-to-one holds ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) let f be PartFunc of C,D; ::_thesis: ( f is one-to-one implies ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) ) A1: f " = f " ; assume f is one-to-one ; ::_thesis: ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) hence ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) by A1, FUNCT_1:32; ::_thesis: verum end; theorem :: PARTFUN2:61 for Y being set for f, g being b1 -valued Function st f c= g holds for x being set st x in dom f holds f /. x = g /. x proof let Y be set ; ::_thesis: for f, g being Y -valued Function st f c= g holds for x being set st x in dom f holds f /. x = g /. x let f, g be Y -valued Function; ::_thesis: ( f c= g implies for x being set st x in dom f holds f /. x = g /. x ) assume A1: f c= g ; ::_thesis: for x being set st x in dom f holds f /. x = g /. x then A2: dom f c= dom g by GRFUNC_1:2; let x be set ; ::_thesis: ( x in dom f implies f /. x = g /. x ) assume A3: x in dom f ; ::_thesis: f /. x = g /. x then f . x = g . x by A1, GRFUNC_1:2; then f /. x = g . x by A3, PARTFUN1:def_6; hence f /. x = g /. x by A2, A3, PARTFUN1:def_6; ::_thesis: verum end;