let f1, f2 be Function of NAT,(union (rng sequence_univers)); :: thesis: ( ( for n being Nat holds f1 . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) ) & ( for n being Nat holds f2 . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) ) implies f1 = f2 )
assume that
A9: for n being Nat holds f1 . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) and
A10: for n being Nat holds f2 . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) ; :: thesis: f1 = f2

now :: thesis: for i being Element of NAT holds f1 . i = f2 . i

let i be Element of NAT ; :: thesis: f1 . i = f2 . i
reconsider i9 = i as Nat ;
f1 . i9 = (UNIVERSE (i9 + 1)) \ (UNIVERSE i9) by A9
.= f2 . i9 by A10 ;
hence f1 . i = f2 . i ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum