let f1, f2 be Ordinal-Sequence; :: thesis: ( dom f1 = dom (g . 0) & ( for a being Ordinal st a in dom f1 holds
f1 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) & dom f2 = dom (g . 0) & ( for a being Ordinal st a in dom f2 holds
f2 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) implies f1 = f2 )
assume that
A3: ( dom f1 = dom (g . 0) & ( for a being Ordinal st a in dom f1 holds
f1 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) ) and
A4: ( dom f2 = dom (g . 0) & ( for a being Ordinal st a in dom f2 holds
f2 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) ) ; :: thesis: f1 = f2
thus dom f1 = dom f2 by A3, A4; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom f1 or f1 . b₁ = f2 . b₁ )
let x be object ; :: thesis: ( not x in dom f1 or f1 . x = f2 . x )
assume A5: x in dom f1 ; :: thesis: f1 . x = f2 . x
then f1 . x = union { ((g . b) . x) where b is Element of dom g : b in dom g } by A3;
hence f1 . x = f2 . x by A3, A4, A5; :: thesis: verum