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
A3: dom f1 = dom f and
A4: for e being set st e in dom f1 holds
f1 . e = ||.(f /. e).|| and
A5: dom f2 = dom f and
A6: for e being set st e in dom f2 holds
f2 . e = ||.(f /. e).|| ; :: thesis: f1 = f2
thus dom f1 = dom f2 by A3, A5; :: according to FUNCT_1:def 11 :: 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 A7: e in dom f1 ; :: thesis: f1 . e = f2 . e
hence f1 . e = ||.(f /. e).|| by A4
.= f2 . e by A3, A5, A6, A7 ;
:: thesis: verum