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

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

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

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

( 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;( 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 ) )

hence
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 )

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;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 that
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;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

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

( 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

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 object 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 ) )

( ( 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 object ; :: 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 )

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;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 that
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;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

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

now :: thesis: for x being object st x in dom g holds

g . x = f . x

hence
g = X |` f
by A8, FUNCT_1:53; :: thesis: verumg . x = f . x

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