let I be set ; :: thesis: for A being non empty set

for F1, F2 being Function of I,A st ( for x being set st x in I holds

F1 /. x = F2 /. x ) holds

F1 = F2

let A be non empty set ; :: thesis: for F1, F2 being Function of I,A st ( for x being set st x in I holds

F1 /. x = F2 /. x ) holds

F1 = F2

let F1, F2 be Function of I,A; :: thesis: ( ( for x being set st x in I holds

F1 /. x = F2 /. x ) implies F1 = F2 )

assume A1: for x being set st x in I holds

F1 /. x = F2 /. x ; :: thesis: F1 = F2

for F1, F2 being Function of I,A st ( for x being set st x in I holds

F1 /. x = F2 /. x ) holds

F1 = F2

let A be non empty set ; :: thesis: for F1, F2 being Function of I,A st ( for x being set st x in I holds

F1 /. x = F2 /. x ) holds

F1 = F2

let F1, F2 be Function of I,A; :: thesis: ( ( for x being set st x in I holds

F1 /. x = F2 /. x ) implies F1 = F2 )

assume A1: for x being set st x in I holds

F1 /. x = F2 /. x ; :: thesis: F1 = F2

now :: thesis: for x being object st x in I holds

F1 . x = F2 . x

hence
F1 = F2
by FUNCT_2:12; :: thesis: verumF1 . x = F2 . x

let x be object ; :: thesis: ( x in I implies F1 . x = F2 . x )

assume A2: x in I ; :: thesis: F1 . x = F2 . x

hence F1 . x = F1 /. x by FUNCT_2:def 13

.= F2 /. x by A1, A2

.= F2 . x by A2, FUNCT_2:def 13 ;

:: thesis: verum

end;assume A2: x in I ; :: thesis: F1 . x = F2 . x

hence F1 . x = F1 /. x by FUNCT_2:def 13

.= F2 /. x by A1, A2

.= F2 . x by A2, FUNCT_2:def 13 ;

:: thesis: verum