let c be Cardinal; :: thesis: for G being _trivial c -edge _Graph
for v being Vertex of G holds
( G .inDegreeMap() = v .--> c & G .outDegreeMap() = v .--> c & G .degreeMap() = v .--> (2 *` c) )
let G be _trivial c -edge _Graph; :: thesis: for v being Vertex of G holds
( G .inDegreeMap() = v .--> c & G .outDegreeMap() = v .--> c & G .degreeMap() = v .--> (2 *` c) )
let v be Vertex of G; :: thesis: ( G .inDegreeMap() = v .--> c & G .outDegreeMap() = v .--> c & G .degreeMap() = v .--> (2 *` c) )
consider v0 being Vertex of G such that
A1: the_Vertices_of G = {v0} by GLIB_000:22;
set f = v .--> c;
A2: v = v0 by A1, TARSKI:def 1;
dom (v .--> c) = dom ({v} --> c) by FUNCOP_1:def 9
.= the_Vertices_of G by A1, A2 ;
then A3: ( dom (v .--> c) = dom (G .inDegreeMap()) & dom (v .--> c) = dom (G .outDegreeMap()) ) by PARTFUN1:def 2;

now :: thesis: for x being object st x in dom (G .inDegreeMap()) holds
(v .--> c) . x = (G .inDegreeMap()) . x

let x be object ; :: thesis: ( x in dom (G .inDegreeMap()) implies (v .--> c) . x = (G .inDegreeMap()) . x )
assume x in dom (G .inDegreeMap()) ; :: thesis: (v .--> c) . x = (G .inDegreeMap()) . x
then reconsider w = x as Vertex of G ;
A4: w = v by A1, A2, TARSKI:def 1;
hence (v .--> c) . x = c by FUNCOP_1:72
.= G .size() by GLIB_013:def 4
.= v .inDegree() by GLIB_000:149
.= (G .inDegreeMap()) . x by A4, Def12 ;
:: thesis: verum

end;

hence G .inDegreeMap() = v .--> c by A3, FUNCT_1:2; :: thesis: ( G .outDegreeMap() = v .--> c & G .degreeMap() = v .--> (2 *` c) )

now :: thesis: for x being object st x in dom (G .outDegreeMap()) holds
(v .--> c) . x = (G .outDegreeMap()) . x

let x be object ; :: thesis: ( x in dom (G .outDegreeMap()) implies (v .--> c) . x = (G .outDegreeMap()) . x )
assume x in dom (G .outDegreeMap()) ; :: thesis: (v .--> c) . x = (G .outDegreeMap()) . x
then reconsider w = x as Vertex of G ;
A5: w = v by A1, A2, TARSKI:def 1;
hence (v .--> c) . x = c by FUNCOP_1:72
.= G .size() by GLIB_013:def 4
.= v .outDegree() by GLIB_000:149
.= (G .outDegreeMap()) . x by A5, Def13 ;
:: thesis: verum

end;

hence G .outDegreeMap() = v .--> c by A3, FUNCT_1:2; :: thesis: G .degreeMap() = v .--> (2 *` c)
set g = v .--> (2 *` c);
A6: dom (v .--> (2 *` c)) = dom ({v} --> (2 *` c)) by FUNCOP_1:def 9
.= dom (G .degreeMap()) by A1, A2, PARTFUN1:def 2 ;

now :: thesis: for x being object st x in dom (G .degreeMap()) holds
(v .--> (2 *` c)) . x = (G .degreeMap()) . x

let x be object ; :: thesis: ( x in dom (G .degreeMap()) implies (v .--> (2 *` c)) . x = (G .degreeMap()) . x )
assume x in dom (G .degreeMap()) ; :: thesis: (v .--> (2 *` c)) . x = (G .degreeMap()) . x
then reconsider w = x as Vertex of G ;
A7: w = v by A1, A2, TARSKI:def 1;
hence (v .--> (2 *` c)) . x = 2 *` c by FUNCOP_1:72
.= c +` c by CARD_2:23
.= (G .size()) +` c by GLIB_013:def 4
.= (G .size()) +` (G .size()) by GLIB_013:def 4
.= v .degree() by GLIB_000:149
.= (G .degreeMap()) . x by A7, Def11 ;
:: thesis: verum

end;

hence G .degreeMap() = v .--> (2 *` c) by A6, FUNCT_1:2; :: thesis: verum