let A, B be set ; :: thesis: for F, G being Function of A,B

for X being set st F | X = G | X holds

for x being Element of A st x in X holds

F . x = G . x

let F, G be Function of A,B; :: thesis: for X being set st F | X = G | X holds

for x being Element of A st x in X holds

F . x = G . x

let X be set ; :: thesis: ( F | X = G | X implies for x being Element of A st x in X holds

F . x = G . x )

assume A1: F | X = G | X ; :: thesis: for x being Element of A st x in X holds

F . x = G . x

let x be Element of A; :: thesis: ( x in X implies F . x = G . x )

assume A2: x in X ; :: thesis: F . x = G . x

hence F . x = (G | X) . x by A1, FUNCT_1:49

.= G . x by A2, FUNCT_1:49 ;

:: thesis: verum

for X being set st F | X = G | X holds

for x being Element of A st x in X holds

F . x = G . x

let F, G be Function of A,B; :: thesis: for X being set st F | X = G | X holds

for x being Element of A st x in X holds

F . x = G . x

let X be set ; :: thesis: ( F | X = G | X implies for x being Element of A st x in X holds

F . x = G . x )

assume A1: F | X = G | X ; :: thesis: for x being Element of A st x in X holds

F . x = G . x

let x be Element of A; :: thesis: ( x in X implies F . x = G . x )

assume A2: x in X ; :: thesis: F . x = G . x

hence F . x = (G | X) . x by A1, FUNCT_1:49

.= G . x by A2, FUNCT_1:49 ;

:: thesis: verum