let f be Sequence; :: thesis: ( S₁[f] implies for alpha being Ordinal holds S₁[f | alpha] )
assume A1: S₁[f] ; :: thesis: for alpha being Ordinal holds S₁[f | alpha]
let alpha, beta be Ordinal; :: thesis: ( beta in dom (f | alpha) implies (f | alpha) . beta = H₁((f | alpha) | beta) )
assume A2: beta in dom (f | alpha) ; :: thesis: (f | alpha) . beta = H₁((f | alpha) | beta)
dom (f | alpha) c= dom f by RELAT_1:60;
then A3: f . beta = H₁(f | beta) by A1, A2;
dom (f | alpha) c= alpha by RELAT_1:58;
then beta c= alpha by A2, ORDINAL1:def 2;
then (f | alpha) | beta = f | beta by FUNCT_1:51;
hence (f | alpha) . beta = H₁((f | alpha) | beta) by A3, A2, FUNCT_1:47; :: thesis: verum