let f, g be Function; :: thesis: ( dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being object st c in dom f holds

f . c = (f1 . c) * ((f2 . c) ") ) & dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being object st c in dom g holds

g . c = (f1 . c) * ((f2 . c) ") ) implies f = g )

assume that

A1: dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) and

A2: for c being object st c in dom f holds

f . c = (f1 . c) * ((f2 . c) ") and

A3: dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) and

A4: for c being object st c in dom g holds

g . c = (f1 . c) * ((f2 . c) ") ; :: thesis: f = g

f . c = (f1 . c) * ((f2 . c) ") ) & dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being object st c in dom g holds

g . c = (f1 . c) * ((f2 . c) ") ) implies f = g )

assume that

A1: dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) and

A2: for c being object st c in dom f holds

f . c = (f1 . c) * ((f2 . c) ") and

A3: dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) and

A4: for c being object st c in dom g holds

g . c = (f1 . c) * ((f2 . c) ") ; :: thesis: f = g

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

f . x = g . x

hence
f = g
by A1, A3, FUNCT_1:2; :: thesis: verumf . x = g . x

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )

assume A5: x in dom f ; :: thesis: f . x = g . x

hence f . x = (f1 . x) * ((f2 . x) ") by A2

.= g . x by A1, A3, A4, A5 ;

:: thesis: verum

end;assume A5: x in dom f ; :: thesis: f . x = g . x

hence f . x = (f1 . x) * ((f2 . x) ") by A2

.= g . x by A1, A3, A4, A5 ;

:: thesis: verum