let f1, f2 be Ordinal-Sequence; ( f1 is increasing & f2 is increasing implies ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing ) )
assume that
A1:
f1 is increasing
and
A2:
f2 is increasing
; ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing )
reconsider f = f1 * f2 as Ordinal-Sequence by A2, Th12;
take
f
; ( f = f1 * f2 & f is increasing )
thus
f = f1 * f2
; f is increasing
let A be Ordinal; ORDINAL2:def 12 for b1 being set holds
( not A in b1 or not b1 in dom f or f . A in f . b1 )
let B be Ordinal; ( not A in B or not B in dom f or f . A in f . B )
assume that
A3:
A in B
and
A4:
B in dom f
; f . A in f . B
reconsider A1 = f2 . A, B1 = f2 . B as Ordinal ;
A5:
B1 in dom f1
by A4, FUNCT_1:11;
dom f c= dom f2
by RELAT_1:25;
then A6:
A1 in B1
by A2, A3, A4;
A7:
f . B = f1 . B1
by A4, FUNCT_1:12;
f . A = f1 . A1
by A3, A4, FUNCT_1:12, ORDINAL1:10;
hence
f . A in f . B
by A1, A6, A5, A7; verum