let f1, f2 be map of T; :: thesis: ( ( for A being Subset of T holds f1 . A = Cl_Seq A ) & ( for A being Subset of T holds f2 . A = Cl_Seq A ) implies f1 = f2 )
assume that
A1: for A being Subset of T holds f1 . A = Cl_Seq A and
A2: for A being Subset of T holds f2 . A = Cl_Seq A ; :: thesis: f1 = f2
for A being Subset of T holds f1 . A = f2 . A

proof

let A be Subset of T; :: thesis: f1 . A = f2 . A
f1 . A = Cl_Seq A by A1
.= f2 . A by A2 ;
hence f1 . A = f2 . A ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum