let f, g be Function of (dom F), the carrier of L; :: thesis: ( ( for x being object st x in dom F holds

f . x = \\/ ((F . x),L) ) & ( for x being object st x in dom F holds

g . x = \\/ ((F . x),L) ) implies f = g )

assume that

A4: for x being object st x in dom F holds

f . x = \\/ ((F . x),L) and

A5: for x being object st x in dom F holds

g . x = \\/ ((F . x),L) ; :: thesis: f = g

hence f = g by A6, FUNCT_1:2; :: thesis: verum

f . x = \\/ ((F . x),L) ) & ( for x being object st x in dom F holds

g . x = \\/ ((F . x),L) ) implies f = g )

assume that

A4: for x being object st x in dom F holds

f . x = \\/ ((F . x),L) and

A5: for x being object st x in dom F holds

g . x = \\/ ((F . x),L) ; :: thesis: f = g

A6: now :: thesis: for x being object st x in dom F holds

f . x = g . x

( dom f = dom F & dom g = dom F )
by FUNCT_2:def 1;f . x = g . x

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

assume A7: x in dom F ; :: thesis: f . x = g . x

hence f . x = \\/ ((F . x),L) by A4

.= g . x by A5, A7 ;

:: thesis: verum

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

hence f . x = \\/ ((F . x),L) by A4

.= g . x by A5, A7 ;

:: thesis: verum

hence f = g by A6, FUNCT_1:2; :: thesis: verum