let f1, f2 be Ordinal-Sequence; :: thesis: ( dom f1 = dom (g . 0) & ( for a being ordinal number 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 number 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
A1: ( dom f1 = dom (g . 0) & ( for a being ordinal number st a in dom f1 holds
f1 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) ) and
A2: ( dom f2 = dom (g . 0) & ( for a being ordinal number 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 A1, A2; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in proj1 f1 or f1 . b₁ = f2 . b₁ )
let x be set ; :: thesis: ( not x in proj1 f1 or f1 . x = f2 . x )
assume A3: 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 A1;
hence f1 . x = f2 . x by A1, A2, A3; :: thesis: verum