let f1, f2 be Ordinal-Sequence; :: thesis: ( 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 ; :: thesis: ex phi being Ordinal-Sequence st

( phi = f1 * f2 & phi is increasing )

reconsider f = f1 * f2 as Ordinal-Sequence by A2, Th12;

take f ; :: thesis: ( f = f1 * f2 & f is increasing )

thus f = f1 * f2 ; :: thesis: f is increasing

let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b_{1} being set holds

( not A in b_{1} or not b_{1} in dom f or f . A in f . b_{1} )

let B be Ordinal; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

( phi = f1 * f2 & phi is increasing ) )

assume that

A1: f1 is increasing and

A2: f2 is increasing ; :: thesis: ex phi being Ordinal-Sequence st

( phi = f1 * f2 & phi is increasing )

reconsider f = f1 * f2 as Ordinal-Sequence by A2, Th12;

take f ; :: thesis: ( f = f1 * f2 & f is increasing )

thus f = f1 * f2 ; :: thesis: f is increasing

let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b

( not A in b

let B be Ordinal; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum