let n be Nat; :: thesis: for a being set holds product (n |-> {a}) = {(n |-> a)}
let a be set ; :: thesis: product (n |-> {a}) = {(n |-> a)}

now :: thesis: for i being object holds
( ( i in product (n |-> {a}) implies i = n |-> a ) & ( i = n |-> a implies i in product (n |-> {a}) ) )

let i be object ; :: thesis: ( ( i in product (n |-> {a}) implies i = n |-> a ) & ( i = n |-> a implies i in product (n |-> {a}) ) )

hereby :: thesis: ( i = n |-> a implies i in product (n |-> {a}) )

assume i in product (n |-> {a}) ; :: thesis: i = n |-> a
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;

now :: thesis: for x being object st x in dom g holds
g . x = a

let x be object ; :: thesis: ( x in dom g implies g . x = a )
assume A5: x in dom g ; :: thesis: g . x = a
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: verum

end;

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

end;

assume A6: i = n |-> a ; :: thesis: i in product (n |-> {a})
then reconsider g = i as Function ;

A7: now :: thesis: for x being object st x in dom (n |-> {a}) holds
g . x in (n |-> {a}) . x

let x be object ; :: thesis: ( x in dom (n |-> {a}) implies g . x in (n |-> {a}) . x )
assume x in dom (n |-> {a}) ; :: thesis: g . x in (n |-> {a}) . x
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: verum

end;

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

end;

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