let A be Ordinal-Sequence; :: thesis: for b, c being Ordinal holds b -exponent (A | c) = (b -exponent A) | c
let b, c be Ordinal; :: thesis: b -exponent (A | c) = (b -exponent A) | c
A1: dom (b -exponent (A | c)) = dom (A | c) by Def1
.= (dom A) /\ c by RELAT_1:61
.= (dom (b -exponent A)) /\ c by Def1
.= dom ((b -exponent A) | c) by RELAT_1:61 ;

now :: thesis: for x being object st x in dom (b -exponent (A | c)) holds
(b -exponent (A | c)) . x = ((b -exponent A) | c) . x

let x be object ; :: thesis: ( x in dom (b -exponent (A | c)) implies (b -exponent (A | c)) . x = ((b -exponent A) | c) . x )
assume A2: x in dom (b -exponent (A | c)) ; :: thesis: (b -exponent (A | c)) . x = ((b -exponent A) | c) . x
then A3: x in dom (A | c) by Def1;
then A4: x in dom A by RELAT_1:57;
thus (b -exponent (A | c)) . x = b -exponent ((A | c) . x) by A3, Def1
.= b -exponent (A . x) by A3, FUNCT_1:47
.= (b -exponent A) . x by A4, Def1
.= ((b -exponent A) | c) . x by A1, A2, FUNCT_1:47 ; :: thesis: verum

end;

hence b -exponent (A | c) = (b -exponent A) | c by A1, FUNCT_1:2; :: thesis: verum