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
now :: thesis: for x being object st x in I holds
F1 . 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;
hence F1 = F2 by FUNCT_2:12; :: thesis: verum