let C, D, E 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 )

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

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

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

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

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

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

( 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

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

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

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

thus
( x in dom f & f . x in dom s implies x in dom h )
:: thesis: verum
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;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

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

h . x = s . (f . x)

hence
h = s * f
by A10, FUNCT_1:10; :: thesis: verumh . x = s . (f . x)

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