let x be object ; :: thesis: for n being Nat
for c being Complex holds ((0* n) +* (x,c)) ^2 = (0* n) +* (x,(c ^2))
let n be Nat; :: thesis: for c being Complex holds ((0* n) +* (x,c)) ^2 = (0* n) +* (x,(c ^2))
let c be Complex; :: thesis: ((0* n) +* (x,c)) ^2 = (0* n) +* (x,(c ^2))
set f = (0* n) +* (x,c);
set g = (0* n) +* (x,(c ^2));
A1: dom ((0* n) +* (x,c)) = dom (0* n) by FUNCT_7:30;
A2: dom ((0* n) +* (x,(c ^2))) = dom (0* n) by FUNCT_7:30;
A3: dom (((0* n) +* (x,c)) ^2) = dom ((0* n) +* (x,c)) by VALUED_1:11;
thus dom (((0* n) +* (x,c)) ^2) = dom ((0* n) +* (x,(c ^2))) by A1, A2, VALUED_1:11; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (((0* n) +* (x,c)) ^2) or (((0* n) +* (x,c)) ^2) . b1 = ((0* n) +* (x,(c ^2))) . b1 )
let a be object ; :: thesis: ( not a in dom (((0* n) +* (x,c)) ^2) or (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a )
assume A4: a in dom (((0* n) +* (x,c)) ^2) ; :: thesis: (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a
A5: (((0* n) +* (x,c)) ^2) . a = (((0* n) +* (x,c)) . a) ^2 by VALUED_1:11;
per cases ( a = x or a <> x ) ;
suppose A6: a = x ; :: thesis: (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a
then ((0* n) +* (x,c)) . a = c by A1, A3, A4, FUNCT_7:31;
hence (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a by A6, A1, A3, A4, A5, FUNCT_7:31; :: thesis: verum
end;
suppose A7: a <> x ; :: thesis: (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a
then A8: ((0* n) +* (x,c)) . a = (n |-> 0) . a by FUNCT_7:32
.= {} . x ;
((0* n) +* (x,(c ^2))) . a = (n |-> 0) . a by A7, FUNCT_7:32
.= {} . x ;
hence (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a by A5, A8; :: thesis: verum
end;
end;