let n be Nat; :: thesis:
let a be set ; :: thesis:

let i be object ; :: thesis:

hereby :: thesis:

assume i in product (n |-> {a}) ; :: thesis:
then consider g being Function such that
A1: i = g and
A2: dom g = dom (n |-> {a}) and
A3: for x being object st x in dom (n |-> {a}) holds
g . x in (n |-> {a}) . x by CARD_3:def 5;
A4: dom g = Seg n by A2;

let x be object ; :: thesis:
assume A5: x in dom g ; :: thesis:
then g . x in (n |-> {a}) . x by A2, A3;
then g . x in {a} by A4, A5, FUNCOP_1:7;
hence g . x = a by TARSKI:def 1; :: thesis:

end;

hence i = n |-> a by A1, A4, FUNCOP_1:11; :: thesis:

end;

assume A6: i = n |-> a ; :: thesis:
then reconsider g = i as Function ;

A7: now :: thesis:

let x be object ; :: thesis:
assume x in dom (n |-> {a}) ; :: thesis:
then x in Seg n ;
then ( g . x = a & (n |-> {a}) . x = {a} ) by A6, FUNCOP_1:7;
hence g . x in (n |-> {a}) . x by TARSKI:def 1; :: thesis:

end;

dom g = Seg n by A6
.= dom (n |-> {a}) ;
hence i in product (n |-> {a}) by A7, CARD_3:9; :: thesis:

end;

hence product (n |-> {a}) = {(n |-> a)} by TARSKI:def 1; :: thesis: