let x be set ; :: thesis: for n being Nat
for c being complex number holds ((0* n) +* x,c) ^2 = (0* n) +* x,(c ^2 )
let n be Nat; :: thesis: for c being complex number holds ((0* n) +* x,c) ^2 = (0* n) +* x,(c ^2 )
let c be complex number ; :: 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:32;
A2: dom ((0* n) +* x,(c ^2 )) = dom (0* n) by FUNCT_7:32;
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 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 (((0* n) +* x,c) ^2 ) or (((0* n) +* x,c) ^2 ) . b₁ = ((0* n) +* x,(c ^2 )) . b₁ )
let a be set ; :: thesis: ( not a in proj1 (((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:33;
hence (((0* n) +* x,c) ^2 ) . a = ((0* n) +* x,(c ^2 )) . a by A6, A1, A3, A4, A5, FUNCT_7:33; :: 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:34
.= {} . x ;
((0* n) +* x,(c ^2 )) . a = (n |-> 0 ) . a by A7, FUNCT_7:34
.= {} . x ;
hence (((0* n) +* x,c) ^2 ) . a = ((0* n) +* x,(c ^2 )) . a by A5, A8; :: thesis: verum

end;

end;