let X be set ; :: thesis: for C, D being non empty set

for f, g 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 C, D be non empty set ; :: thesis: for f, g 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 f, g 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 )

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

for f, g 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 C, D be non empty set ; :: thesis: for f, g 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 f, g 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 that
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;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

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 object st x in dom g holds

g . x = f . x

hence
g = f | X
by A4, FUNCT_1:46; :: thesis: verumg . x = f . x

let x be object ; :: 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;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