let f1, f2 be Function; :: thesis: ( dom f1 = dom f & ( for e being set st e in dom f1 holds
f1 . e = ||.(f /. e).|| ) & dom f2 = dom f & ( for e being set st e in dom f2 holds
f2 . e = ||.(f /. e).|| ) implies f1 = f2 )
assume that
Z1: dom f1 = dom f and
Z2: for e being set st e in dom f1 holds
f1 . e = ||.(f /. e).|| and
Z3: dom f2 = dom f and
Z4: for e being set st e in dom f2 holds
f2 . e = ||.(f /. e).|| ; :: thesis: f1 = f2
thus dom f1 = dom f2 by Z1, Z3; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 f1 or f1 . b₁ = f2 . b₁ )
let e be set ; :: thesis: ( not e in proj1 f1 or f1 . e = f2 . e )
assume Z5: e in dom f1 ; :: thesis: f1 . e = f2 . e
hence f1 . e = ||.(f /. e).|| by Z2
.= f2 . e by Z1, Z3, Z4, Z5 ;
:: thesis: verum