let F be Function; :: thesis: for X being set holds Card (F | X) = (Card F) | X
let X be set ; :: thesis: Card (F | X) = (Card F) | X
A1: dom ((Card F) | X) = (dom (Card F)) /\ X by RELAT_1:61
.= (dom F) /\ X by CARD_3:def 2
.= dom (F | X) by RELAT_1:61 ;

now :: thesis: for x being object st x in dom (F | X) holds
((Card F) | X) . x = card ((F | X) . x)

let x be object ; :: thesis: ( x in dom (F | X) implies ((Card F) | X) . x = card ((F | X) . x) )
A2: dom (F | X) c= dom F by RELAT_1:60;
assume A3: x in dom (F | X) ; :: thesis: ((Card F) | X) . x = card ((F | X) . x)
hence ((Card F) | X) . x = (Card F) . x by A1, FUNCT_1:47
.= card (F . x) by A3, A2, CARD_3:def 2
.= card ((F | X) . x) by A3, FUNCT_1:47 ;
:: thesis: verum

end;

hence Card (F | X) = (Card F) | X by A1, CARD_3:def 2; :: thesis: verum